OOPSLA（CCF A）（共 737 篇）
2026171 篇 · 10(OOPSLA2)
贝叶斯程序分析引导的 LLM 告警消解
提出由贝叶斯程序分析引导 LLM 判断中间事实并剪枝依赖告警的静态分析告警消解框架，兼顾质量与 token 开销。
Planning to Hammer：面向 Rocq 证明自动化的难度感知分解
Quarry 将证明规划与执行分离，用 LLM 提出分解并由难度模型排序，递归调用 CoqHammer 提升 Rocq 证明自动化。
智能体软件系统的过程中心分析
提出 Graphectory 图编码智能体轨迹的时序与语义关系，实现以过程为中心的分析与在线监控，提升问题解决率。
面向可满足性模理论、Oracle 与自然语言的 LLM 辅助不可满足性证明
首个能为含闭盒函数调用的 SMT 公式生成不可满足性证明的求解器，借助 LLM 从自然语言文档猜想辅助引理。
基于集中不等式的概率浮点舍入误差分析
提出在 FPTaylor 的 Taylor 展开上应用集中不等式的概率浮点舍入分析方法，可高效生成概率阈值。
面向浮点调试的精确残差计算
通过改进无误差变换的残差计算并提出多次重执行的 residue override，在保持效率的同时大幅减少浮点调试误报。
Beer：通过探索-利用实现贝叶斯程序分析中的交互式告警消解
将探索-利用权衡引入贝叶斯程序分析，利用告警结构相关性提升交互式告警排序与消解效率。
1001 行代码的故事：潜在运行时错误引导的规约合成用于验证大规模程序
提出 Preguss，以潜在运行时错误引导静态分析与 LLM 分治合成过程间规约，实现千行级程序的高自动验证。
带用户标注采样语句与 while 循环的概率程序的静态因子分解
为含用户标注采样语句与 while 循环的概率程序给出静态因子分解与程序切片，并据此加速概率推断优化。
将路径重构为逻辑：面向漏洞检测的语义分段方法
SEVDF 用污点分析提取候选路径、再由 LLM 做语义分段与可行性确认，高效检测 C/C++ 路径敏感漏洞。
Prosecutor：贝叶斯反事实故障定位
提出误差传播图与反事实实验的贝叶斯故障定位方法，在 Defects4J 上显著优于基线。
ML GPU 内核的等价性检查
提出首个 GPU 内核等价性检查器，形式化验证手工、LLM 与编译器优化的 ML 内核正确性。
GitHub 上的浮点使用：静态类型语言的大规模研究
首个跨 GitHub 静态类型语言的大规模浮点使用实证研究，并发布千万级真实浮点函数数据集。
用正则表达式跟踪借用
提出以正则表达式跟踪访问路径的借用检查类型系统，经 Lean 机械化并部署于 Sui 的 Move 字节码验证器。
面向机器学习内核的符号化基本块剖析
提出符号化程序剖析，用输入相关的符号公式代替动态插桩计算 ML 内核基本块计数，中位加速约 1.5 万倍。
面向 Isabelle/HOL 神经定理证明的极简证明语言
提出极简证明语言 Minilang，并翻译 Isar 语料微调 LLM，以提升 Isabelle/HOL 神经定理证明性能。
SymGPT：结合符号执行与大语言模型审计智能合约
提出 SymGPT，用大语言模型把 ERC 规则翻译为 DSL 并由符号执行自动检测智能合约违规。
OBsmith：LLM 驱动的 JavaScript 混淆器测试
提出 OBsmith，用 LLM 生成程序草图并结合等价与蜕变测试，自动发现 JavaScript 混淆器的语义保持缺陷。
noDice：面向带非确定性与条件化的离散概率程序的推断
提出 noDice，扩展 Dice 以对含非确定性与条件化的离散概率程序进行推断，并用决策图缩减所构造 MDP 的状态空间。
从相似度排序到确定性判定：LLM 增强的源码到二进制函数定位
提出 XLoc，用 LLM 将源码转为伪反编译表示并提取差异摘要验证，实现源码到二进制函数的确定性定位。
T-REX：教导大型语言模型用言语化执行语义进行推理
提出教师-学生框架 T-REX，用逐步自然语言执行语义理由训练小模型预测程序状态，超越 GPT-4o。
分离逻辑的系统化设计
提出从程序语义系统推导内嵌局部性原理的局部公理与框架规则的方法。
Datalog 程序的自动化调试
将派生事实视为测试用例、证明树视为执行谱，把 SBFL 迁移到 Datalog，实现无需人工交互的故障规则定位。
面向 Maven 项目的基于 Agent 的漏洞自动修复
提出 Remedius，用 LLM 智能体结合 SMT 优化统一依赖升级与补丁移植，修复 Maven 项目依赖漏洞。
概率程序的类型导向离散化
提出类型导向的全局变换 Slice，将连续概率程序精确离散化，保持语义并赋能离散推断引擎。
形式化 Linux eBPF 核心 ISA：机器化操作语义及其真实世界应用
在 Rocq 中形式化 eBPF 核心 ISA 的全部 153 条指令，并据此验证 eBPF 验证器抽象域的可靠性、发现内核缺陷。
从对称样本学习对称不变式
提出对称决策树SDT及Horn-SDT方法，从对称样本学习对称不变式，加速参数化程序验证。
SART：神经网络验证中二元变量约简的符号-绝对值重构理论
提出 SART 理论，打破不稳定 ReLU 神经元与二元变量的一一对应，从编码源头降低神经网络完备验证的复杂度。
Phaedrus：利用轻量级生成模型与 LLM 预测动态应用行为
提出 Phaedrus，用 LLM 与轻量生成模型预测动态函数调用，指导免执行、输入特定的编译优化。
P4-SpecTec：将语言机械化框架集成到真实世界 P4 规范中
提出 P4-SpecTec，用可执行算法推理规则机械化 P4 静态/动态语义，生成类型检查器与解释器，发现 24 个 bug。
InspectCoder：通过交互式 LLM-调试器协作实现动态分析驱动的自我修复
首个让 LLM 智能体主动操控调试器、通过交互式动态分析定位并修复复杂逻辑错误的程序修复系统。
面向常数时间分析的反编译
揭示反编译与分析变换会消除CT违规，提出CT透明性并构建CT-RetDec验证工具。
面向现代硬件的可编程分治-合并推断的概率编程
Upix 是首个把分治-合并（DCC）推断实现为框架的概率编程系统，可将通用模型拆分并编译到加速器上高效推断。
动态释放信息流策略的健全强制执行
提出首个健全强制执行动态释放信息流策略的类型系统，形式化证明其可靠性并实现 Rust 原型。
BackSmith：一种系统化的编译器后端测试方法
提出黑盒编译器后端测试方法 BackSmith，通过生成后端导向、抗优化和稀有汇编程序，在 GCC/LLVM 后端发现 104 个新缺陷。
通过跨理论近似验证优化 SMT 求解器
提出跨理论近似方法并实现 Iris，通过理论间最优解一致性检测 OMT 求解器缺陷。
实到仿生成：通过约束求解从真实世界数据合成场景程序
提出 R2SGEN 框架，以解耦 SMT 约束求解从真实世界数据合成结构化场景程序，克服组合爆炸并优于 LLM 基线。
SPONGE：面向在线值流查询的自适应边界锚定索引
提出两阶段边界锚定索引框架，加速在线值流查询并减少冗余搜索与 SMT 调用。
将迭代数据流分析机械翻译为代数程序分析
提出将迭代数据流分析机械翻译为代数程序分析的方法，保证正确且性能更优。
LLM 驱动的深度学习库静默缺陷模糊测试：面向通用且可控的缺陷迁移
利用 LLM 从历史缺陷报告提取并迁移缺陷模式，为相似 API 合成带 oracle 的测试，实现深度学习库静默缺陷模糊测试。
MetaSpace：面向具身智能体空间认知的蜕变测试
提出 MetaSpace，用蜕变测试和 Prolog 编码的蜕变关系自动检测具身智能体的空间认知错误。
EditFlow：通过重构开发者编辑流来基准测试与优化代码编辑推荐系统
EditFlow 从开发者心流视角基准测试并优化代码编辑推荐系统，显著提升顺序重构与推荐精度。
基于高效关系链接的上下文无关语言可达性
提出关系链接视角与 Squid 算法，消除 CFL 可达性求解中的冗余链接操作，显著提升可扩展性。
通过语义三角测量减少 LLM 生成代码中的幻觉
提出语义三角化，将问题变换为需不同算法的离解变体并检查独立解一致性，以降低 LLM 代码幻觉。
从张量加速器 ISA 描述自动生成 ML 编译器后端
提出 ACT，仅凭张量加速器 ISA 描述自动生成集成 XLA 的 ML 编译器后端，性能媲美或超越商用后端与手写库。
Scala 的一等精化类型
为 Scala 3 设计一等精化类型，使精化与子类型、推断、模式匹配统一整合，并机化证明核心演算的类型可靠性。
超越名义性：结构子类型下更快的快速类型分析（RTA）
提出 Kumo，用方法索引与并行化加速结构子类型语言中的 RTA 调用图构建，Uber Go 服务中位加速 116×。
基于 E-graph 的代码体积最小化最优函数内联新方法
将最优函数内联归约为 E-graph 提取，提出代码体积优化算法，比现有调优法快 20 倍且可互补。
通过运行时抽象解释进行随机测试
把随机输入生成重构为抽象域元素的迭代精化，用运行时抽象解释实现轻量约束求解与传播，从而对复杂前置条件的 C 程序做随机测试。
AADT：抽象抽象数据类型
提出开放格与 AADT，以可组合抽象变换器支持结构化值的关系与分离推理，提升抽象解释精度。
确定不可达性：面向依赖漏洞的约束引导可达性分析
提出 ConVReach，以约束引导的静态与动态结合方法判定 C/C++ 依赖漏洞可达性，显著减少误报漏报。
超越覆盖率：使用大语言模型进行自动测试套件增强以提升有效性
提出以存活变异体为引导的全自动 LLM 测试套件增强方法，显著提升变异得分并减少代码生成评估的假阳性。
基于概率编程的量子蒙特卡洛估计
提出 QPPL 语言与编译器，将概率程序编译为量子线路，以加速蒙特卡洛估计并保证语义保持。
CapOpt：面向能力感知的超级优化，生成安全且可证明更快的代码
首个将 capability 语义纳入搜索空间与正确性模型的超级优化框架，在 CHERI 上同时提升性能与内存安全。
SmartFuzz：利用大语言模型与特征组合为数据库模糊测试生成高质量种子
用 LLM 从官方文档与历史崩溃输入中提取 SQL 特征，合成高质量种子以提升 DBMS 模糊测试效果。
多宽度参数化位向量的可靠且完备求解：基于原则性归约
将多宽度参数化位向量归约为单宽度公式，实现可靠完备的高效求解与自动机判定。
面向有副作用 E-graph 的高效提取
提出 Statewalk DP，无需外部求解器即可高效完成有副作用 E-graph 的保序提取，并证明其按 statewalk width 可 tractable。
从演示中合成图查询
提出结合图挖掘与演绎剪枝的图查询合成方法，实现工具 DMiner，可从用户的计算演示中高效合成图查询。
寻找进一步优化的证据：通过编译器原生分析检测遗漏的优化
提出利用编译器原生分析检测遗漏优化，在LLVM上发现31,616处机会并推动20个问题修复。
翻译式分离逻辑验证器中的可靠状态编码
提出首个支持非平凡状态编码的翻译式分离逻辑验证器可靠性形式化框架，并以 Isabelle/HOL 机器化验证。
当 FPGA 遇上数据流分析：一次探索性尝试
提出 FpgaFlow，首个用 FPGA 专用硬件加速过程内集合式数据流分析的设计，借助分配性实现线性空间可扩展并取得平均 12–15 倍加速。
代码–测试协同翻译：面向真实世界程序的实用且有效的程序迁移
提出代码–测试协同翻译问题与CoTTrans框架，用测试一致性指标提升LLM程序迁移的准确性与稳定性。
全自动测试定理
提出一种全自动、鲁棒于等价表述的定理性质测试策略，把生成器搜索建模为约束调度问题。
将基础验证引入真实世界的 Rust 代码
扩展 RefinedRust 以支持 trait、闭包和迭代器等高级抽象并与 unsafe 代码结合，从而对真实 Rust 代码进行基础验证。
面向优化动态信息流控制的类型系统
提出流敏感类型系统 MinIF，静态消除动态 IFC 的运行时检查与标签跟踪开销，并保持程序行为与执行决策不变。
Async/Await 的设计空间探索
系统梳理 straight-line asynchrony 的九维设计空间，揭示看似相同的 async/await 在语义上的分歧。
从节点中心视角重新审视路径覆盖追踪
提出节点中心视角，以线性时间最优算法选取最少基本块进行插桩，大幅降低路径覆盖追踪开销并提升 fuzzing 漏洞检测效率。
使用自动机验证 Repeat-until-Success 协议
提出基于层同步树自动机的全自动框架，验证 RUS 量子协议的功能正确性并发现文献中的新 bug。
EUFⁿ：未解释函数等式理论的一个可判定扩展
将 EUF 扩展为支持参数化复合深度的 EUFⁿ，并用条件同余图给出可判定性与复杂度上界。
用效应系统对抗供应链攻击
提出效应安全的包升级与效应感知包管理器，借助效应锁文件阻止供应链攻击。
使用 isorecursive 用户定义谓词和 magic wand 的分离逻辑规约的溯因推断
提出支持 magic wand 与 isorecursive 谓词的溯因推断，为 Viper 推断循环不变式及辅助操作，可覆盖 80% 以上内存安全规约。
TensorRocq：在 Rocq 中实现图示推理
为 Rocq 提供基于字符串图的张量范畴等价推理与重写工具。
面向指针分析的基于早期汇流对象合并的堆抽象
提出 Valve 堆抽象，通过合并早期汇流堆对象，在不依赖特定客户端的前提下兼顾指针分析效率与高精度。
无穷关系逻辑
提出首个可验证无穷程序族关系性质的 Hoare 风格分离逻辑 IRL，并在 Lean 中实现。
从事件日志中进行增量式程序合成
提出增量式合成算法，从系统自动收集的事件日志中合成 API 调用自动化脚本，并实现工具 LogLoom。
面向更快翻译验证的时空分解
提出按空间与时间两轴分解翻译验证问题，利用编译器信息提升可扩展性，验证更多翻译并加速。
紧凑且表达力强的量子电路优化的合成
提出 QSymb，自动合成紧凑且具形式保证的量子电路重写规则，显著减少两比特门数量。
直接操作与自然语言编程，终能兼得？
提出以编辑语言为共享接口、结合直接操作与自然语言的编程框架，并实证发现用户仍偏好直接操作。
对能力进行分类（Classifying Capabilities）
提出树状、可扩展的 capability 分类器，按语义角色过滤捕获集并支持可判定的不相交推理，在 Scala 3 中实现并于 Lean 4 机器化验证。
2D 光栅化的语义
提出 Skia 2D 图形库的形式语义 μSkia，并在 Lean 中机械化，用于验证并优化 Chrome 生成的光栅化指令。
ZSafe：在零知识中证明专有硬件设计的安全性
提出首个零知识框架 ZSafe，在不泄露专有硬件设计的情况下向验证者证明其形式安全性。
编译 WebAssembly 混合执行：结合分阶段（Staging）、续延与快照
将具体语义分阶段编译为 CPS 混合执行器，并用快照复用避免重复执行，在 WebAssembly 上平均加速 44.9 倍。
使用可组合递归模式与变换进行编程
提出 CRPT：可组合递归模式与变换，将递归类型定义用于无回溯的线性时间识别与变换，并给出类型系统与实现。
通过非预期收益验证智能合约的经济安全性
提出经济模型 CMod 与 Solidity 验证工具 CSol，通过证明不存在非预期单笔交易收益来验证 DeFi 合约的经济安全。
PLEX：精化类型的规范化
提出 PLEX，在 PLE 基础上支持 η-展开、β-归约与依赖模式匹配的符号求值，弥补精化类型与一阶 SMT 求解器间的高阶推理缺口。
Hermes：使路径敏感指针分析可扩展以支持稀疏值流分析
通过符号化内存副作用构建惰性符号表达式图，按需生成过程间值流，大幅加速路径敏感指针分析与缺陷搜索。
RAT-CAT-SAT：内存一致性模型的模型检测
提出 RAT-CAT-SAT，用关系逻辑可满足性与循环证明系统对 CAT 内存一致性模型进行模型检测。
IRIDIUM：一个面向 JavaScript 程序的静态优化框架
提出首个将 JavaScript 系统化降级为结构化中间表示以支持静态分析与优化的框架。
Diatom：带数据流摘要与类型感知 IR 链接的多块化二进制提升
提出多块化并行二进制提升器 Diatom，用数据流摘要与类型感知 IR 链接保可靠性，平均加速 7.45×。
当生命周期解放时：面向 arena 的高阶可达性追踪类型系统
提出统一处理多种生命周期、粒度与共享方式的资源类型系统，用可达性类型追踪个体与成组资源，并在 Rocq 中证明类型与内存安全。
LARTS：面向实时与安全系统的语言抽象
提出 LARTS，用执行域、确定性内存契约与通信通道将实时、隔离与内存安全提升为可验证的语言抽象。
当规范遇上现实：揭示以太坊基础设施中的 API 不一致性
提出 APIDiffer，首个规范引导的以太坊客户端 API 差分测试框架，自动检测跨客户端实现不一致。
使用动态调用树调试调试信息
通过对比优化与未优化程序的动态调用树，系统分类调试信息缺陷并归因于编译器或格式。
驯服九头蛇：面向动态符号执行的目标化控制流变换
提出一种非语义保持但失败保持的编译期控制流变换，消除昂贵符号分支以提升动态符号执行的可扩展性。
用推测传递风格证明或证伪 Spectre 安全性
提出 Speculation-Passing Style 程序变换，将推测常量时间验证可靠完备地归约到常量时间验证。
从裸指针到内存安全：面向 Rust 的模块化需求驱动类型状态分析
提出 Pincer：基于 IFDS 的模块化、需求驱动类型状态分析，精准检测 Rust unsafe 代码中的 use-after-free 与 double-free。
DeCo：一种支持泛型数据类型的增量函数式编程核心演算
提出 DeCo 核心演算，支持泛型数据类型的静态增量函数式编程，并在 Lean 中机械化证明其可靠性。
用 cuFuzz 大规模猎捕 CUDA 缺陷
提出首个 CUDA 导向的模糊测试器 cuFuzz，通过全程序模糊测试、设备端覆盖率反馈与 sanitizer 解耦，发现 43 个未知 bug。
CMakeSonar：一种基于细粒度类型系统的 CMake 缺陷静态检测方法
提出首个静态精准检测 CMake 脚本语义缺陷的方法，通过细粒度类型系统与流敏感分析发现构建配置错误。
可靠且完备的基于不变式的堆编码
提出时间索引堆不变式，借助未解释谓词与预言变量将堆程序验证归约为整数程序验证，并首次同时实现可靠性与完备性。
Mixtris：面向混合选择多方消息传递的机械化高阶分离逻辑
提出首个混合选择多方消息传递的高阶分离逻辑 Mixtris，并在 Rocq/Iris 中机械验证其可靠性与实例。
基于目标中心种子选择与生成的高效定向混合模糊测试
提出 TACO-Fuzz，通过目标中心的种子选择与生成改进定向混合模糊测试，到达目标位置最高约 10 倍加速并发现 17 个新漏洞。
基于单调不动点复用的高效增量 GR(1) 合成
提出增量 GR(1) 合成，通过复用获胜区域与单调不动点加速可实现性检查。
Specy：从事件轨迹中学习分布式系统规约
提出 Specy，从分布式系统事件轨迹中自动学习带事件量词的规约，并支持不变式推导与运行时监控。
面向基础设施即代码引擎的蜕变测试
提出 EMIaC，用 e-graph 生成等价 IaC 程序并检查蜕变关系，以测试 Terraform、Pulumi 等 IaC 引擎。
支持异常与效应的自动资源分析
首个支持异常与效应处理器间非局部控制转移的自动资源界分析，扩展了基于类型的 AARA。
面向带生命周期借用的全自动类型推断
提出带生命周期借用的纯函数语言及全自动类型推断，并可按需插入引用计数以保证可类型化。
PRDT：使用复制数据类型实现共识协议的可组合设计与验证
提出协议复制数据类型 PRDT，用 RDT 单调累积知识实现共识协议的可组合设计与自动安全验证。
Deegen：面向动态语言的可生成 JIT 的虚拟机生成器
提出 Deegen 元编译器，可从 C++ 字节码语义自动生成高性能解释器与基线 JIT 的两层 VM。
Scylla：将 C 的一个应用式子集翻译为安全 Rust
通过类型导向翻译与基于 split tree 的静态分析，把结构化 C 子集编译为不使用 unsafe 的安全 Rust。
集合论类型的实现
提出模块化的集合论类型表示，并重访子类型与 tallying 算法，评估优化与设计选择。
ReFun：重建 EVM 字节码中的函数边界
通过渐进式精化从 EVM 字节码中恢复私有函数边界，精度 94.3%、召回 95.5%。
Release/Acquire 一致性下的 RGSep
证明 RGSep 程序逻辑在 release-acquire 弱内存一致性下仍然可靠，提供更简单的 RA 程序验证方法。
更快失败：面向高性能 PBT 的分阶段（staging）与快速随机性
用多阶段编程消除 PBT 生成器抽象开销并优化随机源，使找 bug 最高提速 13 倍。
交互式数据分析：活类型化表格
提出 Hazel Lab，将渐进类型的标签化元组表与 live typing、rich probes 结合，使表操作支持数据依赖的列模式并保留编辑器支持。
Timeline：为电子表格增加时间维度
提出 Timeline，为电子表格引入离散时间维度，并用 dataflow、coeffect 等 PL 技术支持时间计算与有界内存。
Augur：预测关系数据存储应用中的视图可串行化违反
提出 Augur，首个支持复杂 SQL 查询且仅报告真正违反视图可串行化执行的动态预测分析。
Bonsai：面向内存受限 DNN 训练的高效且最优自动张量重计算
提出算子分段抽象与分段 ILP，使张量重计算在保持最优性的同时扩展到真实 DNN 模型。
干净与脏辅助量子比特的量子逆计算
统一形式化干净与脏辅助比特的逆计算，证明存在性检查为 coNP-hard，并提出与实现合成方法 RwUn。
传递、抽象与类多态的不可变性
提出 PICO 类型系统，用 readonly 引用与 viewpoint adaptation 支持传递、抽象及类多态不可变性，并证明类型可靠性与状态保持保证。
Pyriscope：基于稀疏硬件事件的精确低开销 Python 控制流追踪
在 CPython 上借助硬件追踪模块与迹剪枝实现精确低开销的控制流追踪，平均开销仅 2.99%。
Filtr：编译生物信息学递推式
提出面向生物信息学递推的 DSL 与编译器，将递推规则与剪枝、调度分离并生成高效 C++ 代码。
构造即收敛的 CRDT 组合
提出五个内建收敛保证的组合子，使 CRDT 组合后天然收敛，并在 Lean 4 中形式化与实现。
编译量子正则语言态
提出面向正则语言态及其补集的量子态制备编译器，以最小化 DFA 到最优 MPS 的中间表示统一简洁规格与资源保证。
迈向晚绑定面向对象系统的简洁绑定语义
用 Id 对象模型统一刻画 Smalltalk 与 Self 的方法绑定语义，并将二者视为不同特例。
分阶段注解何时保持语义？机械化带 let 插入的类型化语义保持多阶段编程
提出两种带效应追踪的两阶段演算，以自动 let 插入保持语义，并机械化证明分阶段程序与其去阶段化版本上下文等价。
面向细粒度微架构观察的语言方法
提出 DSL 与事件追踪框架 HT，通过地址布局指定微架构效应并连接软硬件事件，支持处理器性能分析。
通过性能剖析理解加速器编译器
提出周期级剖析器 Petal，让加速器设计语言的程序员理解编译器决策如何影响生成硬件的性能。
Granthi：基于酉线路连线的高阶量子编程
提出纯酉高阶量子语言 Granthi，让量子程序成为可传递、相干复合的一等值并编译为静态量子电路。
基于递归不变式的分阶段多步 UTXO 工作流
提出递归不变式与三值 DSL，在 UTXO 上实现分阶段多步工作流并证明验证可靠。
Wasm 3.0 并发模型的形式化刻画
为 Wasm 3.0 的 struct 提出并发语义，证明编译方案与优化正确，建立 DRF 性质并提供模型检测工具。
面向可扩展变体与深层模式匹配的 trait 模块化类型安全
提出支持可扩展变体、深层模式匹配、方法重写、穷尽性保证与独立类型检查的 trait 语言，实现模块化类型安全。
面向组合搜索的半声明式语言
提出半声明式语言 SetLah!，用分层块表达组合搜索并编译到 ASP，兼得模块化与高效求解。
类型、能力与效应系统：关于纯度、语义与表达力的视角
提出基于上下文等价的纯度语义基线与完备度表达力度量，证明效应与能力系统不可比较，并综合出兼具优势的类型-能力-效应系统。
Geo：面向图模式挖掘的查询重写框架
提出可编程查询优化框架 Geo，用重写规则与等价饱和自动组合图模式等价，并保持结果正确与可重构。
带词法追踪的差分执行
提出词法追踪为差分执行步骤提供稳定标识，并在Rocq中验证带缓存的差分执行语义，实现渐进高效。
Lawyer：高阶非直谓并发分离逻辑中基于义务（obligation）的模块化活性推理
提出 Lawyer，首个支持模块化高阶非直谓活性规约的机械化程序逻辑，用纯逻辑标记迁移系统嵌入义务，避免辅助代码插桩。
通过控制非确定性 API 行为检测不稳定测试（flaky tests）
ChaosAPI 通过系统扰动 Java 标准库中非确定性 API 的行为，主动检测多种类型的不稳定测试。
CLower：通过冗余内存访问检测编译器悲观化缺陷
提出黑盒工具 CLower，通过随机 C 程序插桩执行检测编译器冗余内存访问（悲观化）缺陷，在 GCC/LLVM 发现 23 个缺陷。
优化流水线中 Profile 信息的自动传播
提出递归比较代码区域 opcode 直方图的轻量方法，在优化流水线中自动传播 profile 信息，比 LLM 与 LLVM/BOLT 方法更准确。
理解并发现 JIT 编译器性能缺陷
首个系统研究 JIT 编译器性能缺陷的工作，提出分层差分性能测试并发现多个未知缺陷。
通过提升定位语法糖的类型错误
提出 Stellar 框架，通过提升核心语言类型规则，在表层语法中精确定位并报告可修复的语法糖类型错误。
多阶段编程的机器化语义
在 Rocq 中机器化验证带效应的多阶段核心演算 λ_run$，证明类型与展开可靠性和阶段区分。
在线输入语法合成辅助的符号执行
提出在线输入语法合成辅助符号执行的方法 Lase，通过语法导向搜索与 token 级语法合成生成合法输入，提升解析与功能代码覆盖。
rank-2 多态函数的类字典特化
提出部分求值优化技术，打破递归 rank-2 多态函数无法进行类字典特化的僵局，并在 GHC 插件中实现显著加速。
Prunario：通过剪枝可能冗余的场景来测试自动驾驶系统
提出 Prunario，利用模拟预测剪枝冗余测试场景，提升自动驾驶系统测试的场景多样性与缺陷发现能力。
混合博弈控制包络合成
提出子值映射与dGL归纳刻画，合成最宽松的混合博弈控制包络。
Call-by-Push-Value 的交换转换与 Join Points
为 CBPV 识别交换转换，定义 CCNF 并给出基于 A-规范化的单遍翻译，用 join point 避免代码复制并证明求值等价。
剥茧抽丝：揭示变异灰盒模糊测试中被抑制的黄金种子
提出 PoCo，通过禁用障碍条件守卫并迭代选择，挖掘被覆盖守卫抑制的黄金种子以提升模糊测试效果。
基于示例与树自动机的文法修复
提出基于示例和树自动机的 CFG 歧义修复方法，可自动生成符合设计者意图且适合解析器生成的文法。
VeriEQ：通过等价电路变换发现 Verilog 仿真器与综合器缺陷
提出 VeriEQ 框架，用等价电路变换生成语义等价的 Verilog 程序，以蜕变测试高效检测仿真器与综合器的行为偏差缺陷。
异步多参与者会话类型中的混合选择
提出支持异步混合选择的多参与者会话类型框架，允许协议状态瞬时不一致但保证最终一致，并实现工具链与 Erlang 案例。
Beacon：通过系统目录一致性验证检测 DBMS 中的失效访问控制漏洞
提出 Beacon，通过验证 SQL 操作与系统目录的一致性来检测 DBMS 中失效的访问控制漏洞。
有效命题（EPR）高阶函数式编程
在高阶纯函数式语言中借助 Extended EPR 与关系抽象实现可判定、支持量词的程序验证，并用三值逻辑隐藏编码复杂性。
类型安全的单调对象演化
提出语言 May，用继承式单调对象演化与仿射权限系统，在允许别名时静态保证对象重分类安全。
函数式与命令式动态语言的类型推断
为同时支持函数式与命令式范式的动态语言提出基于集合论类型的类型系统与推断方法。
RandSet：面向模糊测试种子调度的随机化语料库缩减
提出随机化语料库缩减技术 RandSet，在缓解种子爆炸的同时实现多样化种子选择并保持低运行时开销。
块测试
提出块测试（block tests），将内联测试从单语句推广到任意代码片段，并为 Java 实现 BDK 工具包。
重新审视集合论类型中的行多态
提出在记录类型构造子内直接支持行变量布尔组合，使集合论类型获得行多态，并实现于 SSTT 与 MLsem。
MGQL：GQL 的可执行小步语义
提出 MGQL：GQL 只读子片段的首个机械化小步操作语义与可靠类型系统，连接 ISO 39075 标准与可执行实现。
Relight：面向分布式任务型系统的简单用户级检查点与快速前向重放
提出 Relight，首个面向分布式任务型程序的自动检查点与快速前向重放框架，几乎无需改动代码即可完成完整作业恢复。
Refined² 环境分类器
为支持可变状态的 MetaML 式多阶段编程提出 Refined² 环境分类器类型系统，静态排除有害作用域逃逸。
TwinString：在 JVM 上用堆外数据保持字符串语义
提出 TwinString，将字符串数据置于堆外，同时保持 java.lang.String 语义与 API 兼容。
揭示垃圾回收隐藏的内存开销
提出结合真实硬件与周期精确模拟的低开销测量方法，量化六种现代 Java GC 对内存系统的隐藏开销。
自顶向下 = 自底向上：通过多参与者全局协议对活性的可靠且完备刻画
证明自顶向下与自底向上多参与者会话类型系统在活性上具有完全相同的可类型化能力。
无稳态性能时代的实验评估方法论
针对虚拟机负载缺乏稳态的现象，提出分段稳态的性能评估方法，并显著降低置信区间失效频率。
Frashokereti：非中止的乐观复制对象
刻画可乐观复制且不中止调用的对象类型ORDT，证明其覆盖CRDT，并给出高效协议Frashokereti。
Speak Now：基于多方会话类型的安全 Actor 编程
提出 Maty，首个支持静态多方会话类型且允许 Actor 参与多个会话的 Actor 语言设计。
为高效内存超额订阅设计 GPU 数据结构
提出双层层次化哈希表与跳表设计，在 GPU 统一虚拟内存超额订阅下提升访问局部性与性能。
面向反应式实体-组件系统的提交窗口观察契约
提出 RxTCoreECS 演算，形式化反应式 ECS 的提交窗口观察契约，并在 Rocq 中机器化验证其核心定理。
编者按
介绍 PACMPL 本期收录 OOPSLA2 2026 的 93 篇论文及首轮 2 篇论文，展现编程语言研究的广度与深度。
2025216 篇 · 9(OOPSLA2)
AutoVerus：为 Rust 代码自动生成证明
提出 AutoVerus，用 LLM 智能体网络自动为 Rust 代码生成 Verus 正确性证明，90%+ 任务成功。
大语言模型驱动的符号执行
提出基于路径分解的 LLM 符号执行方法，用代码表示泛化路径约束让 LLM 直接推理，并实现轻量、语言无关的 AutoBug 引擎。
Laurel：用大语言模型解除自动验证的阻塞
Laurel 利用大语言模型自动生成 Dafny 断言，通过错误定位与代码库示例提示，减少验证器所需人工提示。
通过软证据在贝叶斯程序分析中融合形式信息与非形式信息
将 Datalog 分析概率化，用神经网络把变量名等非形式信息编码为软证据，以改进报警排序。
论贝叶斯程序分析的抽象精化
提出基于条件独立性的抽象精化方法，用反例引导按需搜索抽象，提升贝叶斯程序分析精度。
混合精度调优中健全性的代价
首次系统评测混合精度调优工具，量化健全静态分析与不健全动态方法在性能收益与精度保证间的权衡。
带天使式假设的开放程序内存安全验证
提出 Seeker，用 LLM 挖掘惯用模式并实例化为天使式假设来补全缺失代码，以高精度区分开放程序内存安全误报与真实缺陷。
保证浮点神经网络分类一致性的量化
提出CoMPAQt用MILP验证量化网络分类不一致性，并给出保证或近似保证与浮点网络分类一致的纠正机制。
Artemis：通过LLM辅助的跨过程路径敏感污点分析实现准确的服务器端请求伪造检测
提出Artemis，用LLM辅助的跨过程路径敏感污点分析检测PHP应用SSRF漏洞，显著降低误报并发现新CVE。
注意抽象鸿沟：将等价饱和引入真实世界的 ML 编译器
将等价饱和用于真实 ML 计算图，结合全局代价模型优化 XLA，在 CPU/GPU 上平均提速 3.45%。
通过资源分解集成资源分析
提出资源分解，将多种资源分析技术组合，并证明组合得到的成本界可靠。
MLIR 中可靠且模块化的自动微分活性分析
将 AD 活性分析形式化为抽象解释并证明其可靠性，在 MLIR 中实现含函数摘要的模块化版本，获得显著加速。
为交互式定理证明合成蕴含引理
基于数据驱动的不变式推断，在 Rocq 中自动合成蕴含形式的辅助引理以减轻交互式证明负担。
量化神经网络中比特翻转攻击的验证
提出首个针对量化神经网络比特翻转攻击的形式化验证框架，可证明其免疫或定位所有脆弱参数。
DNN 认证器健全性的自动验证
提出 ProveSound，通过符号化 DNN 将 DNN 认证器的健全性验证归约为 SMT 可处理问题，实现任意架构认证器的自动验证。
反例潜力引导的神经网络高效增量验证
提出基于反例潜力的增量神经网络验证方法 Olive，优先重验更可能含反例的子问题以尽早发现反例。
连续概率程序演绎验证的基础：从勒贝格到黎曼再返回
提出用黎曼和近似积分，将连续概率程序的期望界验证归约为 SMT 不变量验证，并证明收敛与 coRE 完全性。
通过编译扩展不确定性之上的优化
提出带分支定界半环的二元决策图IR，将概率优化编译为可扩展的推断与优化流程。
通过 iDP 验证守护神经网络分类器的仅标签访问隐私
LUCID 用形式化验证计算 iDP 确定性界，只对不满足 iDP 的标签加噪，以极小精度损失守护标签访问隐私。
带相关输入的概率 Datalog 推断
提出 Praline，扩展 Datalog 以在输入事实相关时进行精确概率推断，并用 δ-exact 算法高效求出紧的概率界。
PReMM：基于LLM的多方法缺陷程序修复——分而治之
提出 PReMM，通过分而治之与双智能体 LLM 生成跨多方法补丁，修复多方法缺陷。
LLVM AArch64 后端的翻译验证
提出 arm-tv，形式化验证 LLVM IR 到 AArch64 汇编的翻译，并在该后端发现 45 个此前未知的误编译缺陷。
深度神经网络的 Mini-Batch 鲁棒性验证
提出按 mini-batch 联合验证多个 ε-球的可靠且完备验证器 BaVerLy，加速 DNN 局部鲁棒性验证。
预测性并发分析的健全性
统一并推广预测性并发分析的健全性定义，提出三步证明模板，并证明六个已有分析（含首个弱内存分析）健全。
用于验证 eBPF 程序的流敏感精化类型系统
提出流敏感精化类型系统，在用户态自动推断 eBPF 验证证明证书，缩小可信基并提升可调试性。
Flix：一种语言集成 Datalog 的设计
提出 Flix 中语言集成 Datalog 的设计，使 Datalog 程序可模块化、多态、类型化地复用于程序分析等任务。
概率程序的结构抽象与精化
提出结构抽象精化框架，将概率控制流自动机抽象为MDP，并用CEGAR复用非概率验证技术验证概率程序阈值问题。
交互式定理证明中战术库的自动发现
提出战术依赖图（TDG）驱动的战术发现方法，自动学习可复用战术并将证明重构得更模块化。
UTFix：使用 LLM 的变更感知单元测试修复
提出 UTFix，用 LLM 结合静态/动态代码切片与失败信息，修复因代码变更而过时的单元测试，恢复断言与覆盖率。
理解并改进 flaky 测试分类
揭示先前 flaky 测试分类评估高估，构建真实数据集并提出训练策略 FlakyLens，显著提升分类性能。
IncIDFA：一种高效通用的增量迭代数据流分析算法
提出通用增量算法 IncIDFA，可精确高效地增量更新任意单调迭代数据流分析。
KestRel：使用E-Graph进行程序对齐的关系验证
提出用E-Graph与等式饱和构造中间程序，并以执行轨迹驱动抽取实现程序对齐的关系验证。
基于参数化安全证明的自适应屏蔽
提出编程语言框架，用参数化安全证明与DSL定义自适应屏蔽，为学习控制器提供概率安全保证。
可综合 Verilog 的仿真语义
指出现有 Verilog 标准与可综合子集语义的不一致，修复并给出首个可执行真实硬件设计的仿真语义形式化。
多语言概率编程
提出 Multi PPL，使精确离散推断与重要性采样两种概率编程语言可靠互操作，并证明推断算法可靠性。
面向神经符号程序合成的主动学习
提出受限共形评估与SmartLabel，使神经符号程序合成在神经组件误预测下仍能通过少量用户交互收敛到目标程序。
LOUD：合成最强和最弱规范
提出 LOUD 框架，为含存在量词的非确定程序同时合成最强 ℒ-推论与最弱 ℒ-蕴含式规范。
反例引导的模块化规约推断
提出反例引导算法，自动推断模块化验证所需的被调函数规约，并在有限与大小受限无限规约空间下给出可靠完备性结果。
面向未来 700 种内存模型的组合符号执行
为可参数化内存模型的组合符号执行平台提供新形式基础，并在 Rocq 中机器化。
面向机器化程序验证的结构化时序逻辑
提出结构化时序逻辑 ticl，将复杂（余）归纳证明编码为结构引理，在证明助手中以高抽象层次对无限程序的安全性/活性进行组合式验证。
Orax：一个反馈驱动的框架，用于高效求解可满足性模理论与预言机问题
提出反馈驱动的 Orax 框架，在 SMT 求解器与 oracle 处理器间闭环反馈 oracle 映射信息，高效求解 SMTO 问题。
基于摘要引导搜索的软件模型检测
提出 GPS：用组合摘要静态分析引导程序状态有向搜索，高效证明安全并发现反例。
MTP：面向 AI 集成编程的意义类型化语言抽象
提出 MTP 范式，用语言级构造从代码语义自动生成提示并处理 LLM 输出，大幅降低开发复杂度。
面向静态分析的快速字节码前端的两种方法
提出模式感知的三地址码翻译与剪枝式类型推断，构建高效且可靠的 Java 字节码前端。
基于类型驱动变异的 C++ 编译器模糊测试
提出首个面向 C++ 类型系统的变异式编译器模糊测试方法 TyMut，通过类型驱动变异与 must 分析发现 102 个编译器缺陷。
零知识中正则表达式等价性的余归纳证明
提出首个正则表达式等价性的零知识证明协议 Crêpe，基于导数与余归纳，可在数秒内验证大规模证明。
通过后向分析揭示（内存）错误来源
提出后向欠近似的 SIL 与 Separation SIL 证明系统，定位错误来源并处理指针与动态内存错误。
CoSSJIT：在JIT编译器中结合静态分析与推测
提出 CoSSJIT，将静态分析与 JIT 运行时推测结合，用于生产 JVM 上的激进栈分配，栈分配提升 5.7 倍。
Carapace：Rust 中的静态–动态信息流控制
首次实现面向现成 Rust 及其未修改编译器的混合静态–动态信息流控制，支持保密性与完整性。
检查数据库系统的可观察正确性
提出以客户端观测为中心的符号编码方法，用 SMT 求解验证黑盒数据库事务的语义正确性与隔离保证。
情境中的 QED：一项针对证明助手用户的观察研究
通过情境访谈观察 30 名 Rocq 和 Lean 用户，揭示证明助手实际使用中的迭代、对话、外部资源与超越 QED 的设计诉求。
通过 Filtered-Simulation 弥合真实世界与形式化二进制提升之间的差距
提出 filtered-simulation 刻画真实二进制提升中启发式假设的正确性，并形式化三种核心变换。
单态化的简单本质
提出基于类型流分析的简单单态化技术，可处理高阶与存在类型，并证明其类型与语义保持。
刻画具有无限状态与数据的全局协议的可实现性
对带无限状态与数据的符号通信协议，给出可实现性的精确语义刻画、检查算法及复杂度结果。
机会式并行 Lambda 演算
提出基于 lambda 演算的机会式求值策略，自动并行分派独立外部调用并流式返回结果，并用 Opal 语言验证。
SafeRace：评估并应对存在数据竞争时的 WebGPU 内存安全
揭示 WGSL 数据竞争可致内存安全护栏被优化删除的规范漏洞，并提出 SafeRace 内存安全保障 SMSG。
交错使用大语言模型进行编译器测试
提出两阶段 LLM 编译器测试框架 LegoFuzz：离线生成小型代码片段，在线组合复用，在 GCC/LLVM 发现 66 个 bug。
DESIL：检测 MLIR 编译器基础设施中的静默缺陷
提出 DESIL，通过 UB 消除、lowering 路径优化与差分测试检测 MLIR 编译器的静默优化错误。
通过生成式等式饱和支持的改写空间探索验证 SMT 重写器
提出 Aries，用拟态变异与生成式等式饱和探索 SMT 重写空间，验证重写系统并发现真实缺陷。
rustc 编译器中的缺陷实证研究
对 rustc 语义分析与 IR 处理阶段 301 个缺陷进行系统实证研究，分类成因并评估现有测试工具。
验证反应式系统中的异步超属性
提出博弈式方法验证反应式系统中的任意 ∀*∃* 异步 HyperLTL 公式，并给出有限状态判定片段与原型实现。
盒子里有什么：面向泛型数据结构的人机工程学与表达力兼备的捕获跟踪
提出 System Capless 与 reach capabilities，使捕获类型能跟踪泛型数据结构内的能力，并在 Scala 3 中实现与验证。
形式化直线运动 G-code：面向制造工具的不变式检查与差分测试
提出将 G-code 提升为长方体集合与近似点云表示的算法，支撑 CAD 不变式检查、切片器差分测试与网格修复评估。
高效的减而治之线性一致性监控
提出减而治之框架，将线性一致性监控归约为识别保线性一致值，并为常见并发数据类型给出多项式乃至近线性时间算法。
基于已验证位爆破的交互式位向量推理
提出首个端到端已验证的位爆破器 bv_decide，将高效位向量推理作为 Lean 交互式证明 tactic，并支持反例生成。
memo：一个用于推理“推理”的领域特定概率编程语言（或：关于 memo 的备忘录）
提出领域特定概率编程语言 memo，以专用语法语义和数组编程推断，支持心智理论建模。
激活函数的凸包近似
提出 WraAct，利用双线性分段函数简化局部几何，高效构造通用激活函数的紧凸包过近似。
DepFuzz：基于函数依赖引导的高效智能合约模糊测试
提出 DepFuzz，用基于距离的函数依赖引导混合模糊测试，高效生成可暴露漏洞的交易序列。
定量时序推断的积构造统一方法
提出基于余代数的统一框架，用分配律刻画系统与时序性质的积构造，并给出用于定量时序推断的充分正确性条件。
检查含积分的实数的 δ-可满足性
扩展 δ-决策过程以处理含积分的实数约束，并实现工具 ∫dReal 支持验证与合成。
程序集合的语义
提出可复用指称语义理论，刻画无限程序集合验证的表达力与组合性，并导出首个可靠且相对完备的 Hoare 式逻辑。
抽象精化引导的程序合成：面向机器人从演示中学习
提出 RoboScribe，从原始连续演示中自动推导状态与动作抽象，迭代精化并合成可解释的机器人控制程序。
基于正则化的图简化实现快速客户端驱动的 CFL 可达性分析
提出 MoYe，用正则近似简化图并剪除无用边，在保证指定点对可达性精确的前提下加速客户端驱动的 CFL 可达性分析。
构造即正确：通过神经网络训练实现经认证的个体公平性
提出由可证明公平的初始化与保公平训练算法组成的框架，在训练全程形式化保证个体公平性。
连续张量抽象：当索引取实数时
提出允许实数索引的连续张量抽象与代数表达式，并为分段常数张量实现存储格式与自动内核生成。
虚拟化内存地址的模态抽象
提出模态断言 [r]P 与虚拟 points-to 断言，在 Rocq 中验证多地址空间 x86-64 虚拟内存管理代码。
从线性到借用
逐步为线性类型演算加入不可变借用、词法生命周期、再借用与可变借用，并用分离逻辑证明其语义类型安全。
基于序维护的增量双向类型检查
提出用顺序维护数据结构实现增量双向类型检查，细粒度编辑后快速传播类型更新，性能较从头重分析快多个数量级。
面向小样本学习的 DSL 合成
研究符号域中小样本学习的 DSL 合成问题，证明其可判定性并给出正则树表征。
宽度无关位向量谓词的已验证判定过程
在 Lean 中机械化模型检测与 MBA-Blast 算法，为宽度无关位向量谓词提供可扩展的已验证判定过程。
正则约束传播的力量
提出并实现正则约束传播方法，可可靠且完备地求解一大类字符串约束，并显著提升 OSTRICH 求解器性能。
验证模式匹配覆盖分析器的可靠性与完备性
提出 Ikaros，用生成器与 SMT 预言机系统验证 Scala、Java、Haskell 模式匹配覆盖分析器的可靠性与完备性。
一种量化量子网络行为的语言
提出 PBKAT，一种面向量子网络 Bell pair 分发协议的概率/可能性行为规约、验证与定量分析语言及工具。
调优随机生成器：将基于属性的测试视为概率编程
把生成器的随机选择权重视为可学习参数，在离散概率编程系统中自动离线优化测试输入分布，显著提升找 bug 效率。
ad hoc 解析器正则文法的静态推断
提出用精化类型推断从无标注 ad hoc 解析器源码中静态推断正则输入文法，并实现 Panini 系统。
结构化信息流：重新审视非干扰的类型
提出结构化信息流类型系统，基于混合逻辑自然地支持解分类，并通过逻辑关系证明非干扰性。
保持非干扰性的优化编译
提出超性质模拟框架，统一刻画编译过程中 k-超性质的保持，并给出可复用的非干扰保持代码变换。
为非线性双曲偏微分方程求解器合成可靠且精确的抽象变换器
提出 Phocus，首个双曲 PDE 求解器的抽象解释，通过合成抽象变换器验证不变式与稳定性。
GALA：一种高性能图神经网络加速语言与编译器
提出 GALA DSL 与编译器，通过两级 IR 组合算子内/间优化并支持训练专用变换，实现 GNN 推理与训练加速。
将 ∀∃ 关系霍尔逻辑编码到标准霍尔逻辑中
提出通用编码理论，把 ∀∃ 关系霍尔逻辑归约为标准一元霍尔逻辑，无需扩展框架或重证可靠性。
面向 GQL 的灵活且富有表达力的带类型路径模式
为 GQL 核心片段提出带不精确类型的类型系统 FPPC，静态检测空查询与卡住查询并保证类型安全。
静态分析 R 程序的数据流
提出面向 R 的静态数据流分析框架，能处理动态特性并生成数据流图，支持程序切片。
RestPi：面向 REST API 的路径敏感类型推断
提出路径敏感类型推断引擎 RestPi，为 Ruby REST API 自动生成更精确完整的响应类型规约。
Metamorph：从 Dafny 规约合成大型对象
提出 Metamorph，利用 Dafny 验证器反例与分段距离度量，将大型对象的长方法调用序列合成化为加权 A* 搜索。
PAFL：利用项目特定的故障模式增强故障定位器
提出 PAFL，通过挖掘项目历史故障模式并设计故障模式描述语言，增强现有故障定位工具。
堆逻辑的 FO-完全程序验证
提出 FO-完全性标准，并给出首个支持隐式 heaplet、可 FO-完全验证的 frame logic 与 separation logic 及 SMT 验证方法。
归纳堆谓词的归纳合成
提出仅用正例的ILP算法，从内存图合成含数据性质（如有序性）的递归分离逻辑堆谓词。
JavART：一种使用从学习方法提取翻译规则的轻量级基于规则的 JIT 编译器
提出用学习提取翻译规则的轻量级JIT编译方法，跳过解释和一级优化直接生成高质量本地代码。
ROSpec：面向基于 ROS 的机器人软件的领域特定语言
提出面向 ROS 的 DSL ROSpec，用于指定并验证机器人组件的配置与集成，检测误配置。
多模态基于草图的行为树合成
提出BtBot，利用自然语言与正反例，通过LLM生成草图并搜索修复，自动合成行为树程序。
浅层量子电路的可扩展等价性检查与验证
提出基于投影的等价性检查 PBEC，可在经典计算机上以对量子比特数线性时间/空间验证浅层量子电路等价性。
面向超安全验证的递归程序乘积
提出递归乘积程序构造框架，将无限状态递归程序的超安全验证归约为标准安全验证。
ApkDiffer：面向 Android 应用的准确且可扩展的跨版本差异分析
提出 ApkDiffer，用两阶段分解对齐实现 Android 应用跨版本方法级差异分析，兼顾精度与可扩展性。
穿越山峰：程序合成中版本空间代数的多路交集
提出多路交集方法，直接合并多个小型版本空间代数，避免中间结果爆炸，显著加速程序合成。
分而治之：一种面向博弈论安全的组合式方法
提出对博弈进行组合式分解的增量安全分析方法，把博弈论安全性化归为 SMT 求解，可扩展至百万节点规模。
Agora：在机密计算验证中减少信任并提升开放性
提出 Agora 框架，通过可委托验证、区块链悬赏和开放断言语言，为机密计算构建可信且开放的验证平台。
基于 Labeled Bunches 的量化欠近似
提出 LabelBI 证明系统，用测试级别量化欠近似保证，从而可靠组合验证与测试等异构分析。
同步行为检查：一种发现遗漏编译器优化的方法
提出同步行为检查（SBC），通过交叉验证多个优化的协同行为来检测编译器遗漏的优化。
论带效应答案类型多态程序的高阶模型检测
提出支持答案类型多态与子类型的效应处理演算 HEPCF□ATM，并通过选择性 CPS 变换证明其高阶模型检测可判定。
面向对称性质的 Hoare 逻辑
提出基于群作用的 Hoare 逻辑，用于验证命令式程序的对称性质，并实现原型工具 SymVerif 发现实际模型错误。
Stencil-Lifting：面向遗留代码中模板核摘要提取的层次化递归提升系统
提出层次化递归提升系统 Stencil-Lifting，自动将遗留代码中的 stencil 核转换为语义等价的 DSL 实现。
P³：通过乘积程序推理补丁
提出P³框架，自动为C语言补丁构造乘积程序，支持复杂补丁并无缝对接AFL++与KLEE进行补丁推理。
迈向崩溃一致性验证
提出 CrashLang 语言与类型系统，保证良类型数据结构实现崩溃一致，并实现编译器验证五个基准。
面向 I/O API 迁移的可靠静态分析方法
提出 Sprout 系统，结合流敏感指针分析与 typestate 分析，自动将程序迁移到新 I/O API 并保证行为等价。
面向 Rust 分布式程序的精化方法论
提出自底向上精化方法，用局部归纳不变式关联抽象模型与 Rust 实现，并可复用现成验证工具。
声明式程序分析中的通用可扩展性（基于 Choice 的组合剪枝）
利用 Datalog 的 choice 构造自适应剪枝关系投影，使既有声明式程序分析框架在几乎不损失完备性下大幅加速。
Pyrosome：面向模块化元理论的验证编译
提出 Coq 中可扩展语义与编译的通用框架 Pyrosome，以归纳式等价保持支持语言特性与编译器增量扩展和垂直组合。
用户自定义聚合的同态演算
提出同态演算，可验证或反驳 UDAF 是否为 dataframe 同态，并构造合并算子以支持增量与并行计算。
迈向有理论支撑且实用的选择性对象敏感指针分析框架
提出选择性对象敏感指针分析理论框架 Moon，通过图可达性识别可提升精度的对象，实现大幅加速且精度损失极小。
通过选择性加宽实现高效抽象解释
提出基于值流分析的选择性加宽，仅对参与值流回边的变量加宽，在保持精度不变的同时大幅加速抽象解释。
Place Capability Graphs：Rust 所有权与借用保证的通用模型
提出 Place Capability Graphs，从 Rust 编译器表示直接提取所有权/借用保证，覆盖超 97% 公开 crate 函数，并支撑验证与分析工具。
增量式认证编程
提出增量认证编程形式框架，定义完成精化与完备性，并在 Rocq 中实现 IncRease 原型。
论形式化验证对软件开发的影响
通过扎根理论访谈14名Dafny用户，分析自动主动验证对大型项目开发的影响与采纳机会。
全局变量及其初始化的模块化推理
提出首个实用的模块化验证技术，基于分离逻辑与模块不变式推理全局变量及其初始化
面向权威 ISA 语义扩展指令选择验证的规模
提出 Arrival，为 Cranelift 生产级 Wasm 编译器验证指令选择，自动化规则链与有状态规则推理，显著减少人工规约。
HieraSynth：面向完全超优化的分层空间分解并行框架
提出分层分解与并行搜索的超优化框架，可在大指令集上完整合成最优程序。
对外部调用的推理
提出用于对象能力与封装限制外部调用效应的断言、规约与 Hoare 逻辑，并证明其可靠性。
高阶程序时序安全效应的抽象解释
提出基于自动机的抽象效应域与类型-效应系统，可扩展地验证高阶递归程序的时序安全性质。
Finch：支持控制流的稀疏与结构化张量编程
提出 Finch 语言，统一控制流与结构化张量表示并协同优化，自动特化控制流到数据，显著加速稀疏张量计算。
更快的显式轨迹监控导向编程：面向软件测试的运行时验证
提出 Lazy MOP，通过惰性存储唯一轨迹等三项优化，显著加速显式轨迹在线 MOP 的软件测试运行时验证。
API 引导的数据集合成用于微调大型代码模型
提出 API 引导的数据集合成框架 DataScope，以 API 覆盖率筛选与合成高质量微调数据，显著提升大型代码模型的微调效果。
期望代价分析的指称语义基础
提出概率程序期望代价分析的指称语义框架 cert，并证明其与操作语义的可靠性和充分性。
代码样式表：面向代码的 CSS
提出“代码样式表”，将 CSS 式选择器推广到 AST，按语义信息对不同粒度的代码显示进行样式化。
QbC：通过构造实现量子正确性
提出 QbC 方法，用前后置条件与可靠完备的精化规则从规约构造正确的量子程序。
SPLAT：面向稀疏规则注意力的优化 GPU 代码生成框架
提出 ACSR 稀疏格式与 SPLAT 代码生成框架，为多样稀疏注意力模式在 GPU 上生成高性能实现。
模态效应类型
提出基于模态效应类型的新方法，无需显式效应多态即可静态保证效应操作均被处理。
Uniform Tokenization 问题的高效算法
提出两种线性时间、低内存的 tokenization 算法，并验证优化版本在实际负载上优于先前方法。
Lilo：面向活性的高阶关系式并发分离逻辑
提出高阶关系式并发分离逻辑 Lilo，支持并发程序活性与终止性的模块化验证，并在 Coq 中机械化。
探索实体-组件-系统模式中并发的理论与实践
提出 Core ECS 形式模型，刻画确保调度无关确定性的 ECS 程序类，并调查现实框架的不足。
高层次抽取与变异：面向 JavaScript 引擎的基于模板的模糊测试
提出 TemuJs，从真实 JS 程序中抽取抽象模板并在模板层做语义感知变异，为 JS 引擎生成多样化且有效的测试用例。
探明剖析器准确性：一种通过机器码级减速近似剖析器准确性的方法
提出机器码级减速构造近似真值，用于评估 JIT 系统采样性能剖析器的准确性。
用模糊测试与形式化严谨性革新量子模拟器
结合 Alloy 形式化的 QASM 3.0 模型与约束引导模糊测试，对量子模拟器做差分基准测试，发现 8 个缺陷（6 个未记录）。
数据流电路的机器化语义
提出数据流电路的机器化操作语义，在 Coq 中证明图与项演算等价并给出确定性条件。
外挂式强一致性：规约、实现与验证
将强复制系统作为弱复制数据存储的应用，并用 Super-V 以局部稳定更新前置条件实现基于 SMT 的共识安全验证。
Python 中基于属性的测试的实证评估
通过 426 个 Hypothesis 程序语料与变异测试，实证评估 Python 中基于属性的测试的找错效果及影响因素。
将量子程序验证嵌入 Dafny
提出 Qafny c，将量子程序验证编译到经典验证器 Dafny，并验证 37 个量子程序。
模型引导的分布式系统模糊测试
提出以 TLA+ 抽象形式模型覆盖率为引导的分布式系统模糊测试算法，更快发现更多缺陷。
闭合循环：支持表达性循环引用的可达类型
扩展可达类型，引入循环引用、浅层限定符跟踪与逃逸规则，提升高阶别名与可变状态表达力并机器验证类型安全。
零开销的词法作用域效应处理器
提出类型制导翻译，使词法作用域效应处理器在无效应时不增加主代码运行时开销，并形式化证明其正确性。
通过跨语言代码生成器与差分测试发现编译器缺陷
提出 CrossLangFuzzer，用统一 IR 生成跨语言 JVM 测试程序并结合变异与差分测试，发现 24 个编译器缺陷。
用 PRISM 增强自动程序修复：一种基于语义的过拟合补丁检测方法
提出 PRISM，用语义特征与定制学习算法检测 APR 过拟合补丁，在保留正确补丁的同时减少误报与审查负担。
Bennet：面向堆操作程序的随机规约测试
提出 Bennet：基于 CN 分离逻辑规约，为堆操作 C 程序自动生成满足前置条件的随机测试输入并发现缺陷。
面向失效安全的轻量级类型与效应系统：基于约束子类型推断追踪永久与临时失效
提出类型与效应系统 InvalML，用布尔代数类型追踪永久与临时失效，无需别名或捕获限制，并提供完备推断算法。
Hambazi：面向增强现实的空间协调合成
提出良构复制数据类型与协议，并自动合成AR空间协调，兼顾低延迟、空间完整性与收敛。
通过 Prophecy Potentials 实现 Rust 的自动线性资源界分析
提出 RaRust，一种利用共享势与预言势的 Rust 类型化线性资源界分析，可处理借用、重借用、堆结构与递归。
Solana 的 eBPF 指令集架构完整形式语义
首次给出 Solana eBPF 字节码的完整小步语义，并在 Isabelle/HOL 中形式化与验证。
以多样化执行揭示 Heisenbug
通过跨插桩密度与硬件平台的多样化执行，构建 WebAssembly 动态数据竞争检测框架 Beanstalk，并提出 heisen factor 度量。
压缩且并行化的结构化张量代数
提出 DASTAC 框架，将张量高层结构传播到低层代码生成，结合布局压缩与多面体优化实现并行张量代数。
Symbolic MRD：动态内存、未定义行为与外在选择
提出首个无 thin-air 的 C/C++ 内存模型，支持别名分析驱动的编译器优化、未定义行为假设和外在选择，并提供高性能可执行工具。
将经典相继式演算编译到常规硬件：编译的对偶性
提出基于经典相继式演算的中间表示，并展示其可直接翻译到常规硬件，给出了形式描述、实现与初步性能评估。
面向动态语言的多态记录
为带集合论类型（并、交、否定）的记录引入行多态，给出子类型判定与类型检查算法，并证明类型系统可靠。
目的地演算：一种用于纯函数式内存写入的线性 λ-演算
提出以 destination 为核心的纯函数式线性 λ-演算，用模态类型管理线性与作用域，并在 Coq 中证明类型安全。
AccelerQ：在量子模拟器上利用机器学习加速量子本征求解器
提出 AccelerQ 框架，将量子本征求解器实现视为黑盒，结合机器学习与遗传算法自动调优超参数以提升精度与效率。
检测与解释上下文无关文法的（非）等价性
提出可扩展框架，用于判定、证明并解释上下文无关文法的等价与非等价，并在教育数据上验证。
为 Rust 实现垃圾回收：终结器前沿
提出并实现 Rust 的 GC 方案 Alloy，首次让既有析构函数自动充当 GC 终结器，并解决由此带来的健全性与性能问题。
MIO：面对输入/输出时的多元宇宙调试
提出支持输入/输出操作的多元宇宙调试方法，并证明其只探索常规执行可达的程序状态。
浮点数自标记
提出 self-tagging：用可逆按位变换将浮点值与类型信息叠加在单字中，避免堆分配且性能影响小。
跨商类型等价性的证明修复
扩展 Rocq 证明修复以支持商类型等价（setoid 实现），并在 Cubical Agda 首次给出内部正确性证明。
React-tRace：理解 React Hooks 的语义——一种操作语义与澄清 React Hooks 的可视化器
为 React Hooks 核心机制提出操作语义，并实现解释器与可视化工具以澄清其行为。
为根基性验证重构 Verilog 语义
提出基于最小不动点的 Verilog 语义，支持周期级求值与模块化推理，并在 Rocq 中证明其与标准调度语义等价。
qblaze：一个高效可扩展的稀疏量子模拟器
提出基于紧凑排序数组表示与可并行量子操作算法的稀疏态向量模拟器 qblaze，在多核上高效扩展。
全覆盖：不完整输入生成器的类型引导修复
提出基于覆盖类型的枚举合成算法，自动修复不完整的属性测试输入生成器，使其能生成所有满足前置条件的输入。
自动验证复制感知线性一致性
提出全自动验证 MRDT 复制感知线性一致性的代数性质与自底向上线性化方法。
展示其为何正确：用交互式运行时比较在程序修复中节省 1/3 调试时间
提出 iFix，通过交互式比较补丁的运行时差异，帮助开发者理解补丁正确性并提升修复效率。
基于代表性测试的可扩展且准确的应用级崩溃一致性测试
提出代表性测试策略，仅探索少量代表性崩溃状态，在保证覆盖率的同时扩展到大应用。
类型保持的扁平闭包优化
提出 Flat-Closure Calculus，用类型保持的闭包表示支持常见闭包优化，并证明类型安全与类型保持。
基于路径不敏感仿真的相似性分析的二进制密码函数识别
提出 BinCrypto，用区间域路径不敏感仿真做代码相似性分析，精准高效识别二进制中的密码函数。
C++ 函数模板的快速约束合成
提出基于轻量级过程间静态分析的 C++ 函数模板约束自动合成方法，可快速生成非平凡约束并缩短编译错误信息。
Peepco：基于批次的一致性优化
提出基于批次的一致性优化方法，静态推断操作集的一致性需求并据此在运行时安全地放松重排序。
语言参数化引用合成
提出从 Statix 类型系统规范自动派生逆查找，并借助作用域图进行语言参数化的具体引用合成，以支持可靠重构。
SafeTree：面向微服务的表达性树策略
提出微服务树形策略语言 SafeTree，并基于可见下推自动机在服务网格上非侵入式动态执行。
编排式快速变更：一等位置（集合）多态
提出首个带类型且支持一等进程名与位置集合多态的编排式语言 λQC，并在 Rocq 中验证其无死锁性。
ABC：通过模型合并迈向通用代码风格转换器
提出ABC框架，用模型合并实现基础与组合代码风格转换，并发布BCC Style数据集和CS4BLEU指标。
使用 CAHP 的堆快照匹配与排序：一种基于前缀树的上下文增强堆路径表示，用于精确与部分路径匹配
提出上下文增强堆路径 CAHP 与前缀树匹配方法，改进 Native Image 堆快照对象映射并重排以减少页错误、加速启动。
通过系统化应用研究与工业最佳实践提升性能
将PLDI'22的LXR垃圾回收器产品化，优化为迄今最快Java通用GC，GC成本近乎减半并总结五条经验。
基于布尔代数的限定类型
提出基于布尔代数的类型限定符，扩展 System F<: 并奠定 Flix 效果系统的形式基础。
Fray：面向 JVM 的高效通用并发测试平台
提出 Fray，用 shadow locking 在不替换 JVM 现有并发原语的前提下实现受控并发测试，支持多种交错搜索算法并显著发现更多并发缺陷。
契约系统元理论 à la carte：契约的迁移系统视角
提出用迁移系统统一高阶契约系统元理论，复用定义与证明，并在 Agda 中机化验证。
TraceLink：连接实现与其经过验证的设计
提出 TraceLink，将执行 trace 映射到经过验证的形式设计，自动检测编译实现与设计之间的偏差。
面向效应处理器的 Dynamic Wind
为词法效应处理器设计并形式化了一种 dynamic wind，在任意控制效应下保持良定义语义与资源括约。
REPTILE：递推方程的高性能分块优化
提出 REPTILE 编译器，将递推方程递归分解为唯一分块并生成与手写库性能相当的 C 代码。
用于分布式死锁检测的正确黑盒监视器：形式化与实现
提出并实现首个形式化、可证明正确且完备的分布式黑盒死锁检测监视器，适用于 Erlang/OTP RPC 应用。
Qunity 中可组合的量子控制流与高效编译
为 Qunity 量子控制流语言实现完整编译器与多阶段优化，高效生成 OpenQASM 3 线路。
带标签监听器的类型外推：面向名义式面向对象泛型的可判定类型一致性的基础
首个可靠完备判定过程：无表达式类型标注、含不规则递归泛型接口的名义式OO程序可验证；标签监听器和类型一致性实现类型外推。
带物化义务的语法补全
提出 tall tylr：用可物化的语法义务抽象多种补全可能，并以 tile 解析演算保证任意输入都能恢复为良构项。
TailTracer：面向生产环境的持续尾部追踪
提出持续尾部追踪，仅保留执行轨迹末段，低开销地在生产环境完整记录函数调用与返回序列。
HybridPersist：面向用户友好且高效的持久内存编程的编译器支持
提出 HybridPersist 编译器支持，以极少标注自动保证持久内存程序的崩溃一致性并提升性能。
重载的简单本质：通过基于流的变分类型检查使特设多态更具代数性
提出基于流的变分类型检查框架，将重载视为选择，统一约束收集、求解与重载消解。
im2im：使用知识图谱方法自动转换内存中的图像表示
提出 im2im，用知识图谱自动生成并执行内存图像表示转换代码，消除视觉编程中的手工类型转换。
Tabby：面向高性能零知识证明电路的合成辅助编译器
提出合成辅助编译器 Tabby，从高层程序自动生成高性能 ZK 电路，提升证明效率并保证语义等价。
补全语法引导变换以提升程序归约
提出结构形式转换 SFC 补全语法引导变换，并设计三种归约方法，显著提升程序归约的最小化与规范化效果。
面向表面码量子架构的依赖感知编译
提出依赖感知的量子电路编译算法，用模拟退火近最优地完成量子比特映射与路由。
代数效应的 Adequacy 再探
为一般（含无穷）代数效应建立基于交互树与单子代数的 CBPV 充分性定理。
一类基于可达性的垃圾收集器的病态案例
证明任何现实的可达性 GC 都存在病态程序，迫使其长暂停或拒绝仍有空间的分配，并建立与动态图连通性的归约。
栈操作计算与相对单子的概念
用 CBPV 与 relative monad 统一低层栈操作效果，并推广 do 记法为 monadic blocks。
HpC：面向混合与移动系统的演算
提出混合π演算 HpC，以对经典π演算的最小保守扩展统一刻画移动通信、普适性与连续物理动力学。
用逻辑关系建模可达性类型：语义类型健全性、终止性、效应安全性与等式理论
用逻辑关系为可达性类型建立语义模型，统一证明语义类型健全性、终止性、效应安全与程序等价。
调试 WebAssembly？给它来点 Whamm 吧！
提出 Whamm：面向 WebAssembly 的可编程插桩框架，结合引擎级探测与字节码重写回退，降低工具碎片化与插桩开销。
MetaKernel：通过统一 MVM 与卷积实现高效加密神经网络推理
提出组合式 FHE 编译器方法 MKR，将 MVM 与卷积分解为可组合 MetaKernel，大幅减少旋转开销并加速加密推理。
HeapBuffers：为什么不直接把二进制序列化格式用作你的托管内存？
提出 HeapBuffers，让 Java 托管内存直接采用 IO 就绪的稠密二进制布局，从而消除序列化/反序列化开销。
面向效应与处理器（effect handlers）的追踪即时编译
首次评估面向效应处理器的追踪 JIT 编译，将 Eff、Effekt、Koka 编译到统一字节码并基于 RPython 实现，分析性能与优化效果。
勘误：PAFL：通过利用项目特定故障模式增强故障定位器
本文是对 PAFL 论文的勘误，更正遗漏的共同通讯作者标注，确认 Minseok Jeon 与 Hakjoo Oh 为共同通讯作者。
从会话类型中借用
提出基于借用的会话类型 API 与 BGV 演算，用有序线性类型和到 PGV 的翻译保证类型安全与无死锁。
通过相异性与守卫子类型解放合并（merge）
提出类型相异性放松 disjointness 约束，并用守卫子类型避免歧义，使 merge 在保持确定性下支持重载与嵌套组合。
Work Packets：一种面向 GC 软件工程、优化与创新的新抽象
提出 Work Packet 抽象统一 GC 任务、内核与调度约束，并以两级工作窃取提升并行与性能。
HEMVM：面向可互操作虚拟机的异构区块链框架
提出 HEMVM 异构区块链框架，统一 EVM 与 MoveVM，实现跨 VM 互操作、工具链兼容与高性能交易。
2024148 篇 · 8(OOPSLA1)
增强静态分析以进行实用缺陷检测：一种 LLM 集成方法
提出 LLift，将静态分析与 LLM 结合，用于检测 Linux 内核中的未初始化使用缺陷。
面向贝叶斯程序分析的抽象选择学习
提出基于学习的数据驱动框架，为贝叶斯程序分析自动选择抽象，以提升其泛化能力。
FPCC：基于链条件检测浮点误差
提出链条件引导搜索触发浮点误差的输入，实现工具FPCC，显著优于ATOMU。
基于学习的静态程序切片方法
提出 NS-Slicer，用预训练语言模型预测完整与不完整代码的静态切片，并用于漏洞检测。
可编程 MCMC 与可靠组合的引导程序
提出基于协程和类型系统的框架，验证可编程 MCMC 中用户引导程序的正确性与可组合性。
WhiteFox：由大语言模型赋能的白盒编译器模糊测试
提出首个利用 LLM 与编译器源码信息的白盒编译器模糊测试器 WhiteFox，用于检测深度学习编译器的深层逻辑缺陷。
用类型化洞为大型语言模型提供静态上下文
将LLM代码生成集成到Hazel的带类型洞环境，通过语言服务器提供静态类型与绑定上下文，显著提升补全质量并证明类型定义上下文最有效。
神经网络全局鲁棒性的验证
提出面向分类器的全局鲁棒性性质与 anytime 验证器 VHAGaR，计算最小全局鲁棒界并显著优于已有验证器。
基于生成函数的循环概率程序精确贝叶斯推断
提出基于生成函数的精确贝叶斯推断，可处理带无界循环的概率程序。
PolyJuice：基于等价饱和重写的张量编译器误编译缺陷检测
提出 PolyJuice，用等价饱和生成语义等价的多样计算图，通过差异测试发现张量编译器的误编译缺陷。
大规模非终止性证明
提出组合式欠近似非终止证明逻辑 UNTer_SL，并实现可扩展分析器 Pulse∞，在数十万行代码库中发现未知非终止缺陷。
评估深度学习模型在基础程序分析任务上的有效性
通过构建 CodeSem 数据集，实证评估四种深度学习代码模型在别名预测与程序等价性预测两个基础程序分析任务上的表现。
QuAC：面向 Python 的快速属性中心类型推断
提出 QuAC，通过收集 Python 表达式访问的属性集合并用信息检索预测类，实现快速准确的类型推断。
概率程序的牛顿式程序分析
提出 NPA-PMA 框架，将牛顿法程序分析推广到含非确定性、非结构化控制流和递归的概率程序数据流分析。
正则语言 Parikh 像的约束求解方法
将正则语言 Parikh 像推理转化为约束求解问题，提出 PC* 演算与工具 Catra，避免显式构造积自动机并显著加速字符串约束求解。
为翻译验证建模局部内存的动态分配与释放
提出局部内存动态分配的执行模型与精化定义，将编译器翻译验证可靠地归约为 SMT 可解的一阶逻辑查询。
TorchQL：面向机器学习完整性约束的编程框架
提出 TorchQL，用查询语言表达并检查 ML 模型与数据集上的完整性约束，提升错误发现效率。
Minotaur：面向 SIMD 的合成超优化器
用程序合成与形式验证为 LLVM 搜索整数/浮点 SIMD 优化，获得实际加速。
Rustlantis：Rust 编译器的随机差分测试
首个面向 Rust 编译器正确性的 fuzzer，通过生成 MIR 程序做差分测试，发现 22 个新缺陷。
稀疏等式图（e-graph）的快速最优提取
针对 e-graph 提取的 NP 难与不可近似性，提出稀疏低树宽 e-graph 的最优提取参数化算法及 Rust 实现。
概率程序资源使用量的定量界
结合代价鞅与定量安全性分析，为概率程序给出期望和尾部资源界，突破非负代价、有界更新与期望有限等限制。
通过基于语法的枚举验证 SMT 求解器的正确性与性能
提出 ET，通过将 SMT 理论语法编译为代数数据类型并借助 FEAT 枚举，系统测试 SMT 求解器的正确性与性能。
使用基于 CFL 的环境变换器提升别名感知 IFDS 分析性能
将域敏感访问路径生成重构为 CFL 并归约为 IDE 问题，显著减少 IFDS 数据流事实数，加速污点分析。
用于组合式微分参数不连续性的分布
提出首个可靠微分参数不连续性的一阶可微语言 Potto，并给出指称语义与支持分离编译的高效实现。
高阶概率程序中期望代价的模态类型论
提出 pλ-amor，用分级模态类型论证明高阶概率程序的期望代价界。
使用符号执行发现 ∀∃ 超属性缺陷
提出扩展符号执行以支持迹量化的全自动方法，用于发现 ∀∃ 超属性的违反。
HardTaint：通过选择性硬件追踪实现生产运行中的动态污点分析
提出 HardTaint，结合静态分析、选择性硬件追踪与并行图处理，使生产运行动态污点分析开销降至约 8%。
让 Formulog 变快：为非常规 Datalog 求值辩护
提出 eager evaluation，替代半朴素 Datalog 求值，大幅加速 Formulog 的 SMT 静态分析。
自动化 Unrealizability Logic：面向无限程序集的 Hoare 风格证明合成
提出首个 Unrealizability Logic 证明合成算法 Wuldo，以语法驱动方式自动验证无限程序集并复用非终结符摘要。
面向上下文无关语言可达性的迭代-纪元在线环消除
提出基于传递性符号的迭代-纪元在线环消除，动态压缩 CFL-可达性图并显著加速静态分析。
通过向量加法系统与归纳势函数实现单调过程摘要
提出以带重置向量加法系统与归纳线性势函数精确摘要递归过程，保证组合性与单调性并提升精度。
通过稀疏傅里叶学习实现 Linux 内核中精确的数据竞争预测
将执行轨迹可行性建模为稀疏布尔函数并用稀疏傅里叶学习求解，提升 Linux 内核数据竞争预测精度与发现数量。
发现 Datalog 引擎中的跨规则优化缺陷
提出增量规则求值方法 IRE，通过对比优化程序与禁用跨规则优化的参考程序，自动检测 Datalog 引擎的优化缺陷。
一种纯需求操作语义及其在程序分析中的应用
提出仅用调用栈和程序点/词法层作为状态的纯需求操作语义，并将其有限化直接导出高阶程序分析。
使用图神经网络提升 Datalog 程序分析中抽象精化的可扩展性
用图神经网络从 Datalog 求解计算构图并为抽象参数打分，缩减 CEGAR 约束求解空间，提升大规模程序分析的可扩展性。
PyDex：使用LLM修复入门Python作业中的缺陷
提出基于代码大模型Codex的自动程序修复系统PyDex，修复入门Python作业的语法与语义错误。
CYCLE：学习自我精化代码生成
提出 CYCLE 框架，让代码语言模型依据执行反馈自我精化错误生成，显著增强自修复能力。
Drowzee：面向大语言模型事实冲突幻觉检测的蜕变测试
提出逻辑编程辅助的蜕变测试框架 Drowzee，自动生成测试用例并检测大模型的事实冲突幻觉。
Cedar：一种表达力强、快速、安全且可分析的授权语言
提出授权策略语言 Cedar，兼顾可读性、快速求值、安全与可分析性，并开源实现。
Plume：高效且完备的弱隔离级别黑盒检查
提出首个高效、完备的弱隔离级别黑盒检查器 Plume，可检测数据库隔离缺陷并生成反例。
结果分离逻辑：带计算效应的正确性与不正确性局部推理
提出结果分离逻辑 OSL，统一支持带计算效应的正确性与不正确性推理，并给出符号执行算法。
Tachis：面向期望代价的带信用额度的高阶分离逻辑
提出 Tachis，一种带概率代价信用（cost credits）的高阶分离逻辑，用于证明概率程序的期望代价上界。
GPU 程序中数据竞争的可靠且部分完备静态分析
提出 GPU 数据竞争检测的真阳性定理与近似分析，实现首个可靠且部分完备的检测器 FaialAA。
VeriEQL：带完整性约束的复杂 SQL 查询的有界等价性验证
提出首个基于 SMT 的复杂 SQL 查询有界等价性验证方法，可证明与反驳查询等价性并生成反例。
HiPy：从 Python 代码中提取高层语义以用于数据处理
将通用 Python 函数转换为程序生成器，执行时生成静态类型 IR，实现高层领域优化与高效 C++ 代码生成。
加权上下文无关语言有序二叉决策图（WCFLOBDDs）
提出带过程调用机制的层次化加权决策图 WCFLOBDDs，在量子线路模拟中兼顾 WBDD 与 CFLOBDD 的优势。
基于内存分割的智能合约实用验证
提出面向 Solidity 生成的 EVM 字节码的内存分割变换，用保守内存与指针分析加速 SMT 智能合约验证。
Hydra：用程序合成泛化窥孔优化
提出 Hydra，用程序合成自动将具体窥孔优化泛化为与位宽无关的通用重写规则，并生成可验证的 LLVM C++ 代码。
Seneca：面向 Java 对象反序列化的基于污点的调用图构建
提出 Seneca，用污点分析与 API 建模为 Java 序列化构建健全调用图，以发现反序列化漏洞路径。
ParDiff：网络协议解析器的实用静态差分分析
提出静态差分分析 ParDiff，通过从多个协议实现中提取有限状态机并用互模拟与 SMT 比较，自动发现协议解析器中的语义缺陷。
在 Must 中模型检测分布式协议
提出 Must 框架，用最优动态偏序归约在主流语言上建模并验证分布式协议。
Multris：分离逻辑中多参与方消息传递的功能正确性验证
提出 Multris 分离逻辑，用多参与方协议一致性验证消息传递与共享内存并发程序的功能正确性。
定量最弱超前置（Weakest Hyper Pre）：通过谓词变换器统一正确性与不正确性超属性
提出定量最弱超前置演算，用谓词变换器统一正确性与不正确性超属性的推理。
Call-by-Push-Value 中的效应与余效应
将效应与余效应追踪引入 CBPV 类型系统，证明其可靠性并在 Coq 中机器化验证。
UniSparse：面向通用稀疏格式定制的中间语言
提出 UniSparse 中间语言，解耦稀疏张量的逻辑结构与内存布局，支持通用格式定制及异构代码生成。
StarMalloc：验证一个现代、加固的内存分配器
用 Steel 分离逻辑验证一个并发、安全加固的内存分配器，可作为 Firefox 等真实项目的即插即用替代。
依赖感知的代码自然度
提出DAN，利用程序依赖图抽取代码行序列以整体度量代码自然度，并验证依赖信息能提升区分与下游任务效果。
面向稀疏张量卷积的编译器支持
提出将仿射下标表达式逐步重写为利用稀疏性的循环的编译方法，为稀疏卷积等生成渐近高效代码。
SMT2Test：从 SMT 公式到有效测试用例
提出将 SMT 公式转换为程序、以可满足性作为测试预言来测试程序验证器的方法与框架。
带类型的多级 Datalog 中间表示及其编译器框架
提出首个通用 Datalog 编译器框架，以可扩展的带类型多级 IR 支持任意前端、逐层优化与多种后端。
在单调语义的程序合成问题中自动实现自顶向下枚举的剪枝
提出单调语义下自动构造区间抽象语义，从而在 SemGuS 中无需手工抽象域即可剪枝。
理解与发现 Java 反编译器缺陷
首个系统研究成熟 Java 反编译器缺陷，并提出差分测试框架 JD-Tester，发现 62 个缺陷。
共享指针分析的 ART：安全且高效地复用指针分析结果
提出 ART 模板，紧凑编码并在校验安全后直接再生流敏感指针分析结果，使消费者免于昂贵不动点计算。
统一加速器生成器的静态与动态中间语言
提出 Piezo，用单一中间语言统一加速器生成器中的静态与动态硬件控制，并支持跨控制风格的优化与转换。
libLISA：x86-64 上的指令发现与分析
libLISA 无需人工编写反汇编器，即可自动发现并分析 x86-64 指令，生成 CPU 特定的形式化模型。
精化类型反驳
提出精化类型反驳，将双向类型检查规则系统化转为失败解释，支持全局精化推断，并实现于 Liquid Haskell 扩展 HayStack。
类型推断逻辑
提出一套逻辑框架，使约束式类型推断与elaboration能在Coq中模块化地机器验证其可靠性与完备性。
崩溃下线性一致性的组合性与观测精化
提出带崩溃的并发计算组合模型和 crash-aware linearizability，并给出首个验证崩溃下线性一致性的程序逻辑。
完全验证的指令调度
提出首个完全验证指令调度的机械化证明库，将证明负担降到交换相邻独立指令的语义保持。
参数化基于通道的进程通信的自动验证
提出将 Go 参数化通道通信片段翻译为核心语言并编码为 Dafny 程序，自动验证无部分死锁并推断前置条件。
语义类型引导的缺陷发现
提出语义类型反驳器，借助符号求值证明函数式程序的语义类型性质不成立，从而发现类型错误。
面向底层代码内存静态分析的依赖名义物理类型系统
提出依赖名义物理类型系统，可嵌入抽象解释器，自动证明底层 C 与机器码的类型安全及空间内存安全。
从可执行解释器合成形式语义
提出从语法与封闭解释器自动合成 CHC 形式语义的 CEGIS 算法，并实现 SynAntic 工具。
计算精确的控制接口规范
提出首个为网络数据平面计算精确且可高效监控的控制接口规范（ci-spec）的算法，并在真实程序中发现 bug。
命令式组合式编程：经双向类型化实现带可变引用的类型安全分配性交集子类型
用双向类型化仅限制引用规则，在保留分配性交集子类型的同时为组合式编程加入可变引用，并机器化验证类型安全。
MEA2：一种面向 Go 的轻量级字段敏感逃逸分析及其指向集计算
为 Go 提出字段敏感并结合指向分析的逃逸分析框架 MEA2，显著减少堆分配且编译开销低于 1%。
CoolerSpace：一种用于物理正确且计算高效的颜色编程语言
CoolerSpace 通过赋予物理量纲的类型系统与等式饱和优化，让颜色编程既物理正确又计算高效。
以参数性推导敏感度
提出用参数性从类型检查直接导出函数敏感度，并在 Haskell 库 Spar 中实现。
面向因果推理的归纳图
提出归纳式因果分离图（CSD），用路径依赖类型形式化 happens-before，并在 Agda 中验证逻辑时钟条件。
参数化验证中 CMP 抽象的机械化
在 Isabelle/HOL 中形式化验证 CMP 抽象与强化方法，并实现自动执行与生成证明脚本的工具 AutoCMP。
面向代码 LLM 的高资源到低资源编程语言知识迁移
提出 MultiPL-T，用半合成数据将高资源语言知识迁移到低资源代码 LLM，并验证微调效果。
当你的基础设施是一个有缺陷的程序：理解基础设施即代码生态系统中的故障
首次系统分析 Ansible、Puppet、Chef 中 360 个 IaC 缺陷，总结其表现、根因、复现条件与修复方式。
Quarl：一种基于学习的量子线路优化器
提出基于强化学习的量子线路优化器 Quarl，通过动作空间分解与图神经网络状态表示，在多数基准上显著优于现有优化器。
Synthetiq：快速且通用的量子电路综合
提出基于模拟退火的通用量子电路综合方法，支持任意有限门集与部分规约，速度更快且更通用。
自动缩减访问控制策略的权限
提出 IAM-PolicyRefiner，基于访问日志合成更严格且符合最小权限的 AWS IAM 策略。
Iris-MSWasm：阐明并机器化验证内存安全 WebAssembly 的安全不变量
为 MSWasm 建立机器化语义与 Iris 推理框架，证明其鲁棒能力安全。
远程直接内存访问的语义：TSO 架构上 RDMA 的操作式与声明式模型
为 x86-TSO 上的 RDMA 并发程序提出三个等价形式模型，填补语义基础空白。
高效量子反计算的模块化合成
提出首个模块化自动合成高效量子反计算的方法，支持表达力强的量子程序并生成正确电路。
Hypra：面向 Hyper Hoare Logic 的演绎程序验证器
提出首个针对同一程序多次执行任意超属性的演绎验证技术，并实现工具 Hypra。
SparseAuto：使用递归循环嵌套重构的稀疏张量计算自动调度器
提出基于递归循环嵌套重构的稀疏张量计算自动调度器，可生成渐近更优的调度与代码。
Wasm-R3：面向真实且独立可执行的 WebAssembly 基准测试的记录-归约-重放技术
首个 WebAssembly 记录-重放技术，从真实网页应用生成真实、忠实且独立可运行的基准测试。
量子控制机器：量子编程中控制流的极限
证明经典条件跳转无法直接提升到叠加态，并给出量子计算机可正确实现控制流的充要条件与量子控制机 ISA。
现实的可实现性：规约可信赖的 ABI
提出用可实现性模型形式化定义语言的 ABI，将高层抽象类型与底层代码相连，并首次形式化库演进。
Cocoon：Rust 中的静态信息流控制
用未修改的 Rust 语言与编译器，通过类型系统与过程宏实现静态信息流控制库，保证非干扰且无运行时开销。
Forge：一种面向形式化方法教学的渐进式工具与语言
提出 Forge：基于 Alloy 的渐进式形式化方法教学工具与语言，支持可视化与测试。
Crabtree：由覆盖率与类型引导的 Rust API 测试合成
提出 Crabtree，结合覆盖与类型引导的合成与模糊测试，为 Rust 库 API 自动生成支持 trait 和高阶函数的测试用例。
基于轨迹信息组合式程序合成的控制流反混淆
提出 Chisel：用轨迹引导的组合程序合成实现通用控制流反混淆，86% 案例还原出原程序。
VarLifter：从 Solidity 智能合约字节码中恢复变量与类型
提出 VarLifter，从 Solidity 字节码精确恢复带类型的变量，提升反编译、审计与 fuzzing 效果。
稀疏数组上形状算子的编译
为稀疏数组语言编译形状算子并融合计算，无需物化中间临时数组，显著加速 reshape、concat 等操作。
Jmvx：面向托管语言的高效多线程多版本执行与记录-重放
提出 Jmvx，首个面向 Java 等托管语言的多线程多版本执行与记录-重放系统，开销低。
带答案类型修改的效应处理程序的高阶模型检测
引入答案类型修改限制，使带代数效应处理器的高阶程序模型检测可判定，并实现验证器 EffCaml。
通过分数唯一性实现函数式所有权
将分数权限与分级类型结合，使 Rust 式所有权和借用平滑融入支持线性、分级类型的函数式类型系统。
分离度：一种面向安全并发的灵活类型系统
提出 System CSC：默认允许别名但在类型中追踪，按需控制别名以静态防止数据竞争。
基于期望性质的跳跃证明：在跳表与安全证明中的应用
提出 EHL 的 hopping 证明规则，将概率程序的期望性质目标归约到相关程序，并在 EasyCrypt 中机验证其可靠性。
AdoB：以原子分布式对象桥接良性共识与拜占庭共识
提出 AdoB 抽象，统一建模良性/拜占庭共识，并在 Coq 中机械验证安全性与活性。
HOL4P4：P4 的机器化小步语义
在 HOL4 中形式化 P4 16 的小步语义与类型系统，支持 extern、并发及体系结构级端到端包处理验证。
A-Normal Form 的低层视角
重新审视 ANF 的底层内涵性质，论证应优先采用 monadic form，只在低层命令式中间表示中做 A-规范化。
基于定点振幅放大的量子程序统计测试
提出用定点振幅放大加速量子程序统计测试，减少测量次数与运行时间且保持统计保证。
PROMPT：一个快速且可扩展的内存剖析框架
提出可扩展内存剖析框架 PROMPT，开发者仅需指定事件和核心逻辑即可快速构建高性能内存 profiler。
带链接操作的经验证无锁会话通道
在Iris中分层验证带链接操作的无锁会话通道，并用Coq机器化证明其高层会话类型规范。
终极条件语法
提出一种支持并行/嵌套匹配与条件模式流动的新型模式匹配语法，可脱糖到无回溯核心并保持语义。
完全同构递归类型
提出完全同构递归类型，以可擦除 cast 编码等值递归类型，消除强制转换开销并简化等价推理。
面向时间有界性质的量子概率模型检测
提出 QPMC，用量子电路编码概率模型检测并以量子振幅估计求解时间有界性质，较 SMC 获二次加速。
PP-CSA：实用的隐私保护软件调用栈分析
提出 PP-CSA，用本地差分隐私扰动软件调用栈，在 Java/Android 程序上兼顾效用、隐私与效率。
Multiverse Notebook：将数据科学家转变为时间旅行者
提出计算笔记本引擎 Multiverse Notebook，支持在状态隔离下时间旅行回溯并用新代码重启。
FlowCert：通过动态分数权限对异步数据流进行翻译验证
提出基于动态分数权限的翻译验证技术，证明异步数据流图与源命令式程序在所有输入和调度下行为等价。
用 Datalog 进行面向对象定点编程
设计 OODL 语言，将对象、动态分派和受控可变性融入 Datalog 式定点语义，并编译到 Datalog。
Mix Testing：指定并测试 C/C++ 原子操作实现的 ABI 兼容性
提出 mix testing 与 atomic-mixer，用于发现不同编译器原子操作映射混合链接时产生的 ABI 兼容性 bug。
融合渐进类型
提出 λ_M^★，将渐进类型与基于交类型的合并算子结合，为支持一等类与动态继承的渐进语言奠定类型基础。
以透明性完善 OCaml 模块
提出 Mω 类型系统，覆盖 OCaml 模块中的 applicative/generative functor 与透明归属，并经 Fω 精化证明其可靠性。
并发对象的场景化证明
提出以交换等价类商刻画“场景”的并发对象线性化证明技术，并可从源码推导候选商表达式。
强化学习中的奖励增强用于分布式系统测试
提出基于奖励增强的强化学习随机测试方法，通过衰减探索奖励与语义路标引导，显著提升分布式协议实现的覆盖率和缺陷发现。
针对宽松内存模型的并发数据结构库自动鲁棒性验证
提出面向 C11 内存模型的自动化归纳技术，验证并发数据结构库在宽松内存模型下相对顺序一致性的鲁棒性。
语法糖的语义提升
提出语义提升框架，可从宿主语言语义与脱糖规则静态派生语法糖的自包含求值规则，并保证正确性与抽象性。
带借用的 typestate 的法则与秩序
提出面向不纯函数式编程、基于有序类型与有序偏幺半群资源类型的 typestate 基础，支持灵活借用并证明类型健全性。
AUTOMAP：使用整数线性规划推断秩多态函数应用
提出用整数线性规划自动推断静态类型数组语言中的 map 与 replicate，兼顾动态数组语言体验与静态类型保证。
Taypsi：面向策略无关的茫然计算的隐私策略静态实施
提出将策略无关的 MPC 程序变换为语义等价且静态实施隐私策略的版本，并在新语言 Taypsi 中实现，消除动态检查开销。
消息观察式会话类型
提出带消息观察会话类型的进程语言 Most，并基于带绑定的迹语义证明类型可靠性与组合性。
限定 System F<:：某些条款与条件可能适用
构建 System F-sub-Q，将高阶有界多态与类型限定符理论结合，并用于引用不可变性、函数着色与捕获检查。
编译稠密与稀疏数组上的递推方程
提出一个将递推方程组按数据结构与调度编译为原生代码的框架，并判定其可解性。
渐进类型语言应当具备警觉性！
提出 vigilance，判定渐进类型语言的检查注入与动态语义是否充分执行静态类型系统，并比较 Natural 与 Transient。
Gradient：经由类型中追踪的对象能力实现渐进式隔离
提出渐进式隔离方法，允许按组件逐步迁移到对象能力模型，并在类型中追踪对象权限以持续获得安全保障。
论静态可变性语言的表达力
提出形式框架统一比较静态可变性语言的表达力，并在 Agda 中机器化验证其可靠性与完备性。
用内联汇编扩展 C/C++ 内存模型
首次为含内联汇编（Intel x86，含非临时存储与存储栅栏）的 C/C++ 提出内存模型，并证明既有编译器优化与映射仍正确。
为一等环境辩护
提出基于环境的小步语义 λE，避免替换，自然支持一等环境并具 Coq 形式化。
识别与纠正编程语言行为误解
整理编程语言行为误解清单与检测工具，并构建自动辅导系统来识别和纠正它们。
词法作用域效应处理器：直接实现
提出词法作用域效应处理器的编译策略，将高层效应处理翻译为底层栈切换，并在 Lexa 中实现与验证。
HybridSA：基于位并行的多模式正则表达式匹配 GPU 加速
HybridSA 是异构 CPU-GPU 多模式正则匹配引擎，通过位并行 NFA 模拟与编译优化显著提升吞吐量。
基于协程的 C 语言效应处理器
提出 libseff：面向 C 的基于协程的效应处理器库，可直接在 C 程序中使用且性能有竞争力。
剖析编程语言学习
通过在 Rust 官方教材中加入交互式测验，大规模刻画语言学习过程并识别难点、改进题目与教材干预。
Persimmon：具有可扩展变体类型的嵌套族多态
提出 Persimmon 函数式系统，以嵌套族多态和可扩展变体类型支持模块化扩展，并证明其类型可靠性。
面向切面的 C 编程语言的设计与实现
设计并实现面向切面 C 语言 Aclang 及其编译器，将成熟 AOP 支持引入 C。
借助 NonSequitur 理解大规模多线程应用性能
提出多线程跟踪压缩方法并实现 NonSequitur，让开发者可大规模可视化分析性能问题。
可中断查询处理的运行时系统：当增量计算遇上细粒度并行
提出 PitStop，一种可中断查询处理的运行时设计，在保持顺序一致性的同时实现细粒度并发，提升负载波动下的查询性能。
让并发数据结构变得简单
提出 Multicore OCaml 库 OBatcher，用隐式批处理与转换函子简化批量并行并发数据结构的设计、实现和使用。
从第一性原理推导依赖类型的面向对象编程
提出一个含对偶片段的依赖类型演算，并用去函数化/再函数化在函数式与面向对象风格间保持类型与语义地转换。
内涵函数
提出内涵函数语言特性，使函数可按定义位置与闭包捕获值定义非应用操作，并扩展出内涵 monad。
Mark–Scavenge：等待垃圾自行退场
提出 Mark–Scavenge 并发 GC 技术，通过延迟搬迁年轻代中稀疏存活对象，减少大量搬迁工作并在 ZGC 上验证。
2023110 篇 · 7(OOPSLA2)
为自动微分合成精确的静态分析器
提出 Pasado，通过直接合成自动微分链式、乘积和商法则复合表达式的抽象变换器，获得比组合标准变换器更精确且可靠的静态分析器。
面向代码优化的具体类型推断：结合机器学习与 SMT 求解
提出结合机器学习与 SMT 求解的具体类型推断，无需类型标注即可优化动态类型 Python 代码。
面向 ML 赋能系统安全的感知契约
提出感知契约，用于刻画神经感知误差并保障基于视觉感知的控制系统安全。
面向少像素攻击的深度学习鲁棒性验证
提出 Calzone，首个对 L0（少像素）对抗攻击给出可靠且完备分析的神经网络鲁棒性验证器。
Outcome Logic：正确性与不正确性推理的统一基础
提出 Outcome Logic，统一正确性与不正确性推理，并证明错误规约可在其自身中证伪。
一种实用的调用图构建「鸡尾酒」方法
将多种精度递增的函数指针解析算法协同编排成工作流，在近似精度下首次把高精度调用图扩展到数百万行 C 代码。
硬件感知的超维计算静态优化
提出硬件感知的静态分析优化框架 Heim，为 BSC 超维计算推导满足精度目标的最小超向量尺寸。
面向概率程序的演绎验证基础设施
提出首个面向概率程序的演绎验证基础设施，用实值逻辑、中间验证语言与最弱前置条件支持期望型性质的自动验证。
可能发散的概率程序的下界
提出不依赖几乎必然终止的新证明规则，为可能发散的概率程序建立终止概率与期望值的非平凡下界。
精确递归概率编程
提出一种概率编程语言，可自然表达递归数据上的递归，并通过类型保证的程序变换实现精确推断。
反例驱动的量词实例化及其在分布式协议中的应用
提出反例驱动的关系抽象与细化方法，避免量词实例化导致SMT求解器发散，并验证共识协议安全性质。
自动分离逻辑验证器中的保持验证的内联
提出首个用于自动分离逻辑验证器的保持验证内联技术，并给出经 Isabelle/HOL 验证的语义条件。
Datalog 程序的交互式调试
提出基于自顶向下小步操作语义的 Datalog 交互式调试器，支持 step-into/step-over，并适配 Soufflé 与 IncA。
Turaco：面向程序神经代理模型训练的复杂度引导数据采样
提出按程序执行路径学习复杂度分配采样比例，并用程序分析判定复杂度以训练神经网络程序代理模型。
面向 SMT 编码的内存模型静态分析
通过内存模型静态分析计算关系边界，并优化 SMT 编码，加速有界模型检测。
Grounded Copilot：程序员如何与代码生成模型交互
首个关于程序员如何与 Copilot 交互的扎根理论研究，发现交互呈现加速与探索两种模式。
Verus：使用线性幽灵类型验证 Rust 程序
提出基于 SMT 的 Verus，用线性 ghost 类型与模式系统验证 Rust 程序的功能正确性。
将 C 翻译为安全 Rust 的别名限制
研究 C 到安全 Rust 翻译中别名分析的限制，并提出编码更精确分析结果的方法，使安全指针引用提升 75%。
通过语义正则表达式合成进行数据抽取
提出语义正则表达式及由少量正负例合成该表达式的学习算法，用于兼顾语法与语义的数据抽取。
使用位向量自动机的正则表达式匹配
提出位向量自动机（NBVA）模型与算法，使含界重复的正则表达式匹配时间与重复次数上限无关，并实现 BVA-Scan 引擎。
用效应处理器延续 WebAssembly
提出 WasmFX，用效应处理器为 WebAssembly 增加类型安全的续延与非局部控制流支持。
Arm® 机密计算架构的验证方法：从安全规约到安全实现
提出结合交互式定理证明、模型检测与并发测试的方法，验证 Arm CCA 中 RMM 的规约与原型实现。
突破语言无关程序约简的 1-极小性极限
提出语言无关框架 Vulcan，通过细粒度程序变换进一步缩小 AGR 约简结果，突破 1-极小性。
通过稳定化求解带长度的字符串约束
提出基于稳定化的字符串约束求解算法，可处理长度约束与不等关系，并集成到 SMT 求解器。
Asparagus：智能合约参数化 Gas 上界的自动合成
用多面体几何与实代数几何定理自动合成智能合约 gas 消耗的参数化上界，并首次给出完备性保证。
基于模板的多项式程序合成的代数几何算法
提出用代数几何定理将基于模板的多项式程序合成直接归约为二次规划，避免量词消去并保持半完备性。
用于灵活内存管理的引用能力
提出基于引用能力的属主类型系统，强制 Verona 中区域隔离，支持对象跨区域与线程移动，且数据访问无需原子操作。
面向非纯高阶语言的图中间表示：以精确效应依赖实现可负担的激进优化
提出结合可达性类型与效应系统的类型化图IR，为含副作用与高阶函数的语言提供精确依赖与廉价激进优化。
为语言无关的演绎程序验证器生成证明证书
为语言无关演绎验证器生成可独立检验的证明证书，以认证每次成功验证的正确性。
利用控制流与调用图的稀疏性实现高效按需代数程序分析
提出按需代数程序分析算法，借助控制流与调用图稀疏性，预处理后每次查询仅需 O(k)。
通过局部化规格实现可解释的程序合成
提出子规格机制，为合成程序局部附加由全局规格与上下文推导的逻辑解释，并验证其性质与用户效用。
把自定义数据结构带入 Datalog
提出 Byods：一种嵌入 Rust 的 DSL，使 Datalog 规则对关系的数据结构表示参数化，从而突破引擎内置表示带来的算法复杂度瓶颈。
编译结构化张量代数
提出 StructTensor，在编译期符号化计算张量结构，并用 STUR 统一表示稀疏与冗余结构，优化密集与稀疏张量代数性能。
求解条件线性递推式以进行程序验证：周期情形
提出条件线性递推式在最终周期情形下的闭式解，并实现生成-验证求解器以验证含条件分支循环。
合成规范
提出自动合成规范的方法与工具 Spyro，在用户给定查询和 DSL 下生成最精确且穷尽的 L-性质。
控制流图的有界路径宽度
证明结构化程序控制流图具有有界路径宽度，并给出线性时间路径分解及更快的寄存器分配算法。
分离逻辑中线性化的证明自动化
在 Iris 中为线性化的上下文精化与逻辑原子性证明开发可扩展的 Coq 自动化，显著减少证明工作量。
Verilog 的本质：一种可处理且经测试的 Verilog 操作语义
提出核心语言 λV，为 Verilog 给出覆盖完整特性、可执行且经测试的操作语义，并解决语义陷阱。
一生的冒险：面向 Rust 的 Extract Method 重构
将 Rust 的 Extract Method 重构分解为函数提升与一系列程序修复步骤，并实现工具 REM。
运行时预防机器学习 API 的软件集成失败
提出运行时中间层 SmartGear，自动检测并转换机器学习 API 的不匹配输出，防止软件集成失败。
具有可判定学习的语言：一个元定理
提出 finite-aspect checkable 语言，并用树自动机元定理统一证明多类表达式学习问题可判定。
使用基于速率的会话类型验证 IoT 设备
提出带周期递归的定时进程演算与基于速率的会话类型，保证 IoT 消息传递的速率正确性，并在 Rust 中实现原型。
Beacons：用于预测和利用动态循环特征的端到端编译器框架
提出 Beacons 端到端编译器/运行时框架，预测动态循环特征并驱动主动调度，提升 HPC 资源并发与吞吐。
面向侧信道攻击的高效掩码防护的组合式验证
提出语言级安全概念与组合策略，实现高效掩码防护的自动化验证并优化AES S盒。
渐进概率 lambda 演算
提出并形式化 GPLC，首个渐进类型的概率 lambda 演算，证明其类型安全并满足渐进保证。
函数式程序性质的一阶完备推理
将函数式程序验证中展开递归定义加SMT无量词推理的启发式，推广为组合一阶理论上的完备推理技术。
Leaf：分离逻辑中临时共享的模块化
提出 Iris 分离逻辑库 Leaf，以 guarding 算子统一临时共享状态，支持模块化并发验证。
Rapid：基于区域的指针消歧
Rapid 利用 profiler 将需消歧对象分配到不同对齐内存区域，使动态指针消歧检查无需访存，降低开销并提升循环优化性能。
用差分集合量化与缓解缓存侧信道泄漏
提出差分集合抽象，支持编译期组合精确推理，并实现同时量化与缓解缓存侧信道泄漏的工具DSA。
资源管理规约的推断
提出基于不动点的资源管理规约自动推断，在 Java/C# 上推断出 85.5% 手写注解且几乎不增加误报。
面向代码模型的解释方法
提出 WheaCha，将代码模型预测归因分解为决定性的 wheat 与其余 chaff，并实现工具 HuoYan。
验证隐私保护协议的不可区分性
提出 F* 库 Waldo，通过网络轨迹不可区分性直接验证隐私保护协议，并发现 TLS ECH 规范缺陷。
初始化全局对象：时间与顺序
提出偏序与初始化时间无关性原则，用可模块化、可区域调优的静态分析保障全局对象安全初始化。
AtomiS：面向实用的以数据为中心的同步
提出 AtomiS，通过接口与字段类型限定和静态分析自动生成并发控制，使数据中心同步更实用。
拜占庭容错算法的随机化测试
提出 ByzzFuzz，通过小范围消息变异注入网络与进程故障，随机化测试拜占庭容错算法实现并发现多个真实缺陷。
Rust 中所有权类型的一个扎根概念模型
通过研究 Rust 学习者的所有权误解，提出流敏感权限概念模型与可视化插件，并改进教材教学。
一石二鸟：通过生成对抗网络提升代码生成与代码搜索
用GAN将代码生成与代码搜索互为生成器与判别器，通过对抗训练实现相互提升。
通过前缀引导执行加速模糊测试
提出前缀引导执行（PGE），在执行前缀显示变异用例难以提升覆盖率时提前终止，从而加速覆盖率引导的模糊测试。
面向浏览器模糊测试的更好语义探索
提出生产上下文敏感文法 PCSG，从 W3C 标准构建并增强文法，以提升浏览器模糊测试的语义覆盖与正确性。
用户可定制的脚本语言转译
提出增量式、可定制且可复用规则的转译方法，实现 Python 到 JavaScript 的 DuoGlot，翻译准确率达 90%。
用块模拟形式化验证优化
提出并集成到 CompCert 的翻译验证框架，借助优化给出的提示，可形式化验证 LCM、强度削减等多种优化。
模块化的基于组件的量子电路合成
提出模块级枚举搜索与剪枝方法，从给定组件门高效合成量子电路，较门级合成提速20.3倍。
免费的 stuttering：FreeSim 模拟技术
提出只需异步进展即可保证可靠性的自由 stuttering 模拟技术 FreeSim，并在 Coq 中机化验证。
按需组合式等价饱和理论探索
提出可编程理论探索 DSL Enumo，以可组合算子引导等价饱和的重写规则推断，并支持免求值的 fast-forwarding 策略。
Melocoton：一种用于验证 OCaml 与 C 互操作的程序逻辑
首个形式化 OCaml FFI 语义并验证 OCaml/C 互操作的多语言程序逻辑，已在 Coq 中机器化。
并发分离逻辑中安全内存回收的模块化验证
在并发分离逻辑中为 hazard pointer 和 RCU 设计模块化抽象谓词，并首次形式验证带内存回收的多个并发数据结构。
以结构化视角机械化会话类型：不依赖线性类型而强制线性
把线性条件嵌入类型判断，用结构上下文在 Beluga 中机械化会话类型及类型保持证明。
双向面向对象编程：迈向对象的程序化与直接操纵
提出首个支持对象程序化与直接操纵的双向面向对象语言，并实现 BiOOP 工具。
贪婪隐式有界量化
提出 F≤b，为有界量化提供隐式多态与类型推断，并证明其可靠、完备且可判定，已在 Abella 中机器化验证。
基于容器使用模式的面向对象敏感指针分析上下文去膨胀方法
提出 DebloaterX，利用容器使用模式识别上下文无关对象，大幅加速对象敏感指针分析且精度损失可忽略。
带类型洞的实时模式匹配
从类型论角度研究带类型洞的模式匹配，并将其实现为 Hazel 的完全实时编程环境。
互递归的 iso 递归子类型
提出带声明子类型的 iso 递归类型核心演算，无需平方级膨胀即可表达互递归与高阶/混合种类子类型，并给出可高效检查的片段。
分组调度的形式化抽象
从编程语言视角为 PIFO 树建立操作语义，并提出跨拓扑编译算法，使逻辑调度行为可在不同拓扑上实现。
从能力到区域：实现词法效应处理器的高效编译
提出将二等能力推断为区域/证据的提升推断翻译，使词法效应处理器高效编译且保持类型与语义。
用于分布式系统验证的消息链
提出基于消息链的自动簿记方法，在消息传递抽象层简化异步分布式系统的验证。
通过高效的问题选择改进 Oracle 引导的归纳合成
提出高效且有效的问题选择器 LearnSy，首次普遍提升 OGIS 求解器性能。
由观测程序相似性引导的归纳程序合成
提出度量程序合成，将观测等价松弛为观测相似，用距离度量聚类程序并经修复缩小搜索空间。
大步语义下的资源感知可靠性
在参数化 grade 代数下为带资源标注的大步语义 λ 演算建立资源感知的类型可靠性，并用余归纳技术完成证明。
Spirea：面向弱持久内存的机器化并发分离逻辑
首个面向弱持久内存模型的并发分离逻辑，并在 Coq 中机器化验证持久数据结构的崩溃安全与线程安全。
函数式大数据查询到 SQL 的自动翻译
提出基于反例引导合成与列式分解的 RDD2SQL，将 Spark 函数式查询自动转译为 SQL 并提升性能。
混合多方会话类型：通过端点投影实现协议规范的组合性
提出混合多方会话类型，用端点投影保持语义地组合多个子协议为全局类型。
Rhombus：无需满屏括号的宏新方案
提出 Rhombus：在 Racket 上用中缀语法实现 Lisp 式宏与语言扩展的多绑定空间方案。
Mobius：合成带有递归与发明谓词的关系查询
提出 Mobius，从数据中全自动合成含递归与发明谓词的关系查询，并用数据溯源加速搜索。
基于偏序分析构建动态系统调用沙箱
提出基于偏序分析的动态系统调用沙箱，随程序执行逐步禁用不再需要的系统调用，降低攻击面。
面向 Hindley-Milner 风格类型与效应系统的快速高效布尔合一
提出基于SVE的混合布尔合一算法并用于Flix，将类型与效应推断开销显著降低，编译吞吐提升1.8倍。
领域专家如何使用嵌入式 DSL
通过情境调查与主题分析，揭示领域专家使用 Mimi（气候变化经济学 eDSL）时的需求与体验。
Mat2Stencil：面向结构化网格上显式与隐式无矩阵 PDE 求解器的模块化基于矩阵 DSL
提出 Mat2Stencil 矩阵 DSL 及编译器，用多阶段编程生成无矩阵 stencil 代码并自动并行化，简化结构化网格 PDE 求解器开发。
高阶 where 解分类的可组合安全定义
用逻辑关系为高阶程序中的 where 解分类构建可组合安全定义，并证明其比已有低阶定义更安全。
函数式语言中的 Fluent API
提出在无函数名重载的函数式语言中借助参数多态与 Hindley-Milner 类型推断实现编译期检查的 Fluent API。
回到直接风格：类型化且紧致
提出有类型直接风格与 CPS 语言及其互译，证明类型保持、操作对应，并刻画互译复合的逆性质。
面向效应处理器的渐进类型
提出渐近类型语言 GrEff，支持从未检查到已检查效应类型的渐进迁移，并证明其可靠性与 graduality 定理。
通过有界区域实现双重无界分布式一致性系统的有界验证
提出值对称与数据饱和归约，将双重无界分布式一致性系统验证降至小有限状态模型检测，并实现工具 Venus。
合成高效的记忆化算法
将记忆化算法合成分解为局部目标函数与记忆化划分函数两个子任务，并联合演绎与归纳方法实现高效合成。
类型安全的动态放置与一等放置值
提出 Dyno 语言，用一等放置值和放置类型并集，在支持动态放置的同时保持类型安全与放置正确性。
布局敏感文法中的自动歧义检测
提出布局敏感文法的有界歧义检测方法，以SMT编码局部歧义并机器化验证，可找出最短歧义句。
Secure RDTs：为离线可用 JSON 数据实施访问控制策略
提出 Secure RDTs，利用服务器投影与写中介，为离线可用 JSON 副本数据实施基于角色的访问控制。
Saggitarius：用于描述语法域的 DSL
提出 DSL Saggitarius 描述上下文无关文法族，并用半环解析与 MaxSAT 从示例数据推断最匹配文法。
P4R-Type：一个经过验证的 P4 控制平面程序 API
提出经过验证的 Scala P4Runtime API P4R-Type，通过静态检查与类型系统排除控制平面操作错误。
性能剖析器如何帮助导航类型迁移
通过数万性能调试场景实验比较17种剖析器引导策略，发现用深度类型消除昂贵边界最有效。
Historia：用消息历史逻辑反驳回调可达性
提出消息历史逻辑，通过逐步精化回调控制流验证事件驱动应用的回调可达性断言。
一个极具表现力的美化打印器
提出 Πe 美化打印器，表达力严格更强、可证明最优、复杂度更优，并用 Lean 验证正确性。
面向 C 语言时序内存安全的胖指针
通过胖指针结合动态键锁检查扩展 Checked C，高效且全面地保障 C 程序的时序内存安全。
进入数据流：为基于约束的类型推断提供更好的类型错误信息
提出用子类型约束刻画数据流，将类型错误解释为错误数据流并展示相关程序位置，改进约束类型推断的错误信息。
AST 与字节码：元编译时代的解释器
通过 RPython 与 GraalVM 实现成对解释器，实证 AST 解释器在元编译系统中与字节码解释器性能相当且内存权衡不同。
重用即时编译的代码
提出通过投机性上下文分派从离线策划的代码库中选取已编译函数版本，以复用 JIT 编译代码，降低动态语言预热开销。
当并发至关重要时：面向行为的并发
提出行为导向并发 BoC，将行为作为统一原语实现原子有序的事务型并发，支持多资源独占访问。
System F<: 的简单引用不可变性
提出 System F<:M，将引用不可变性作为 System F<: 的简单扩展，并证明其安全。
结构子类型作为参数多态
系统比较结构子类型与参数多态的表达力，证明完整子类型无法由多态编码，但若干受限子类型可以。
TASTyTruffle：参数多态的即时特化
TASTyTruffle 解释带类型的 TASTy IR，通过类型具体化和 JIT 特化泛型代码，提升参数多态性能。
MemPerf：剖析内存分配器导致的性能下降
提出首个无需对比其他分配器即可定位分配器所致性能下降的 profiler，基于堆对象生命周期区分慢管理与慢访问。
202292 篇 · 6(OOPSLA2)
使用无误差变换的快速影子执行以调试数值错误
提出 EFTSanitizer，用无误差变换作为 oracle 快速影子执行，检测并调试数值误差。
高阶自动微分的抽象解释的通用构造
提出一种通用构造，可将高阶自动微分的抽象解释归约为对实值直线程序的抽象推理。
用不正确性逻辑在大程序中发现真实 bug
基于不正确性逻辑与分离逻辑的融合 ISL 实现自动分析器 Pulse-X，在 OpenSSL 中发现 15 个真实内存错误。
基于 GNN 的作业调度器的可扩展验证
提出 vegas，首个可扩展验证基于 GNN 的作业调度器单步与多步性质的形式化框架。
面向浮点程序的无 Oracle 修复合成
提出基于微结构的动态无 Oracle 方法，自动合成修复以显著降低浮点程序数值误差。
概率循环的时刻已经到来
提出全自动静态分析，为一大类概率循环精确推导程序变量高阶矩，无需外部不变式或模板。
Halide 语言的端到端翻译验证
提出 Halide 端到端翻译验证算法，用 prophetic 注解和 refinement 映射证明生成代码正确。
为上下文敏感程序分析索引扩展 Dyck-CFL 可达性
将扩展 Dyck-CFL 可达性转化为普通图可达性，并借索引实现上下文敏感数据流分析的近常数时间查询。
面向交互式证明的数据驱动引理合成
提出数据驱动的引理合成方法，将交互式证明中的辅助引理生成归约为程序合成，并实现为 Coq 策略 lfind。
从示例合成代码质量规则
提出 RhoSynth，利用开发者代码变更示例自动合成一阶逻辑代码质量规则，并部署于 Amazon CodeGuru Reviewer。
使用神经引导程序合成自动将命令式代码转译为函数式代码
提出基于归纳程序合成与神经引导的命令式到函数式 API 代码转译方法，工具 NGST2 显著优于多个基线。
合成抽象变换器
将抽象变换器的构造视为程序合成问题，可自动生成最精确的抽象变换器，并已在 AMURTH 中实现。
加权编程：一种用于规约数学模型的编程范式
提出加权编程范式及 Dijkstra 风格的 wp/wlp 演算，用以规约并推理超出概率分布的数学模型。
驯服上下文无关语言可达性中的传递冗余
提出 POCR，利用传递关系有序性与混合图表示，在 CFL 可达性求解中高效消除传递冗余并保持精度。
基于 Farkas 引理的可扩展线性不变式生成
提出两项改进，显著提升基于 Farkas 引理的仿射程序线性不变式生成的扩展性。
未选择的路：探索被编译器错过的基于别名分析的优化
提出 Scout，通过约束分配大小与对齐实现单次内存访问的运行时指针消歧，解锁被编译器错过的循环优化。
面向带最小不动点一阶逻辑的模型引导归纳引理合成
提出用有限一阶模型作为反例引导，合成带最小不动点一阶逻辑中的归纳引理以证明公式有效性。
低代码公式语言的神经符号修复
提出 LaMirage，融合符号与神经技术修复低代码公式语言中的最后一英里错误，在真实基准上超越基线。
面向高效流式概率编程的半符号推断
提出半符号推断，使运行时自动实现 Rao-Blackwellized 粒子滤波，精确优先、必要时采样。
Seq2Parse：神经符号式的解析错误修复
结合神经网络预测相关纠错规则与符号纠错解析器，自动修复解析错误。
BFF：位域操作程序的基础化与自动化验证
提出 BFF，在 Coq 中机械化地对位域操作的 C 系统代码实现既自动化又有形式语义基础的正确性验证。
AnICA：分析微架构代码分析器中的不一致
提出 AnICA，用差分测试与抽象解释系统分析微架构代码分析器之间的不一致并归纳原因。
覆盖率引导的联合 IR-Pass 变异张量编译器模糊测试
提出 Tzer，通过联合 IR 与 pass 变异和覆盖率反馈对 TVM 张量编译器进行模糊测试，发现 49 个新缺陷。
MLstruct：结构类型布尔代数中的主类型推断
提出 MLstruct，在结构记录、等递归类型与一阶并/交类型下实现主多态类型推断。
SHARP：面向 Java 的快速增量上下文敏感指针分析
提出首个支持代码增删的上下文敏感增量指针分析算法 SHARP，兼容 k-CFA 与 k-obj，并可高效并行化。
面向随机化程序的符号执行
提出可处理随机抽样的符号执行方法，能在未知输入下验证随机化程序的概率性质与期望值。
经验证的量子 oracle 编译
提出 Coq 中实现的高保障框架 VQO，形式验证从 OQIMP 到 OQASM 再到 SQIR 的量子 oracle 编译器，并用 QFT 降低量子比特开销。
弥合分布式系统定性与定量模型之间的语义鸿沟
提出从非时间非概率分布式系统模型到概率时间模型的自动变换，并证明语义一致性，使定性与定量分析共享同一模型。
类型指导的自然语言查询到可视化合成
将自然语言查询转为 refinement 类型规约，并用类型指导合成生成符合用户意图与设计准则的可视化程序。
面向多个近似神经网络快速认证的证明迁移
提出 FANC，首次在原始网络与多个近似版本间迁移鲁棒性验证证明，显著加速认证。
Satisfiability modulo fuzzing：SMT 求解与模糊测试的协同组合
提出 Sādhak，将模糊测试与 SMT 求解协同用于含闭盒函数的约束求解。
CAAT：一致性作为一种理论
提出一族可刻画多种内存一致性模型的逻辑理论及通用高效求解器，并用于有界模型检测。
面向并发程序验证的 SMT 求解中的一致性保持传播
提出一致性保持的预防式传播方法，使并发程序验证的 SMT 序理论求解可省略一致性检查与冲突子句生成。
将认知原则应用于模型查找器输出：负信息的正面价值
通过受控实验与出声思维，研究模型查找器输出中一次展示实例数量及展示负实例的价值。
面向大规模系统验证的线性类型
将线性类型与SMT验证结合并集成到Dafny，可显著减少内存推理的证明量与验证时间。
语言参数化的静态语义代码补全
基于语法与静态语义规约，语言参数化地合成可靠且完备的代码补全建议。
面向健壮性的必要性规约
提出 Necessity 语言，用必要性算子刻画时序蕴含，从功能规约推导健壮性规约并在 Coq 中机械化验证可靠性。
极不合逻辑，Kirk：即便契约破损、类型不健全且 linter 过多，也能大规模发现类型不匹配
提出 Scotty，将 DefinitelyTyped 的类型声明转为契约并绑定到库与测试套件边界，通过运行测试检测类型与 JavaScript 代码的不匹配。
无界分离逻辑中的分数资源
提出允许断言求值期间持有超过完整权限的无界分离逻辑语义，统一语义与语法乘法并恢复分配、提取与合并性质。
非严格语言中的等价性检查
提出基于符号执行与余归纳的演算，自动证明非严格函数式程序等价并生成反例。
免费的增量类型检查：用作用域图派生增量类型检查器
从 Statix 类型系统规范自动派生增量类型检查器，借助作用域图查询依赖只重分析受影响单元。
为隐式监视器合成细粒度同步协议
提出从隐式监视器合成细粒度显式同步协议的静态分析与 MaxSAT 方法，生成可媲美专家手写的协议。
通配符需要见证保护
提出存在类型见证保护机制，形式化核心演算并证明可靠，可避免 Java 通配符不健全性且误报极少。
量子计算平台中的缺陷：一项实证研究
首个对量子计算平台缺陷的大规模实证研究，揭示量子特有缺陷的分布、表现形式与反复出现的模式。
Elipmoc：以太坊智能合约的高级反编译
提出面向下一代合约分析的以太坊反编译器 Elipmoc，以事务敏感性、路径敏感参数推断等技术大幅提升精度与可扩展性。
基于半环字典的函数式集合编程
提出半环字典这一纯函数式集合抽象与静态类型语言SDQL，统一数据库与线性代数优化，高效处理混合工作负载。
C4：已验证的事务对象
提出 C4 形式验证框架，统一证明事务对象与 STM 库的线性化与可串行化，并在 Coq 中机器化。
论量子程序的不正确性逻辑
提出量子程序的不正确性逻辑，为静态查错提供可靠完备的逻辑基础。
效果、能力与盒子：从基于作用域的推理到基于类型的推理，再返回
提出 System C，将能力与效果系统统一起来，并用盒式值恢复二等值限制，支持完整效应处理器并证明可靠性。
Katara：基于验证提升合成 CRDT
提出 Katara，从顺序数据类型实现自动合成并验证 CRDT 设计，降低正确构造 CRDT 的门槛。
Solidity 智能合约中的内联汇编研究
对以太坊 680 万份 Solidity 智能合约进行大规模实证研究，揭示内联汇编的使用率、演变与模式。
通过 3C 将 C 转换为 Checked C
提出基于静态分析的半自动移植工具 3C，为遗留 C 程序推断 Checked C 检查指针类型与数组边界注解。
Overwatch：学习代码编辑序列中的模式
提出 Overwatch，从 IDE 编辑轨迹中学习编辑序列模式，结合时间上下文预测开发者下一步编辑。
组合式证明超安全性
提出 LHC 逻辑，以超三元组作为统一组合构件，实现更强的 hypersafety 证明组合性。
分离逻辑中基于操作的 CRDT 的模块化验证
在分离逻辑中提出模块化框架，用可靠因果广播库简化 op-based CRDT 实现的安全性质验证，并在 Coq 中机器化验证 12 个实例。
C++ 中的高层效应处理器
提出 cpp-effects 库，在带手动内存管理的 C++ 中实现带类型的高层效应处理器，并验证其性能竞争力。
基于合成的智能合约数据类型重构优化
提出通过数据类型重构并用程序合成自动生成功能等价的合约，以降低 gas 消耗。
量化最强后条件：一种用于推理量化信息流的演算
提出量化最强后条件演算，支持非确定性含循环程序，用于推理量化信息流并导出部分不正确性逻辑。
ST monad 的纯度：通过语义类型化回译实现完全抽象
形式化证明在简单类型 call-by-value lambda 演算中加入 ST monad 后保持纯度，并用语义类型化回译证明完全抽象。
内在类型化的定义式解释器 à la carte
提出基于内在类型化解释器的语言片段抽象，以低代码量实现类型安全语言组件的模块化机械验证。
复杂度引导的容器替换合成
提出 Cres，结合静态分析与复杂度引导的合成，为程序中每个容器方法调用自动选择时间复杂度更低的容器实现，在保持行为的同时提升运行性能。
解析随机性
用自由生成器统一随机生成与解析，证明生成器可分解为解析器加选择序列分布，并借助导数实现带前置条件的数据生成。
效应处理器的一等名称
提出将效应处理器名称作为一等值，并借助 scoped effects 与 rank-2 多态防止名称逃逸的命名处理器设计。
带有未来与历史的并发程序逻辑
提出面向细粒度乐观并发程序的分离逻辑，支持无需幽灵代码的归纳性质与事后历史推理，并实现自动化验证。
基于属性引导合成的神经架构搜索
提出 αNAS：在程序属性抽象空间中搜索神经架构，并用合成过程具体化为网络，显著减少参数与计算量。
动态稀疏张量代数的编译
提出一种编译技术，将动态稀疏张量代数运算编译为适配多种指针式动态稀疏格式的高效代码。
渐进参数性的可辩护封存
提出可辩护封存机制与中间语言 Funky，使渐进参数性同时满足参数性与渐进性且不破坏 System F 等价。
从带副作用的库中进行规范引导的组件式合成
提出用 Hoare 前后条件表达库效应，以双向搜索和冲突驱动学习引导组件式程序合成。
Solo：一种轻量级的差分隐私静态分析
提出 Solo 类型系统，无需线性或关系细化类型即可静态强制差分隐私，并可嵌入 Haskell。
一束会话：通道式并发中束蕴含逻辑的命题即会话解释
提出πBI，用束蕴含逻辑解释会话类型，以spawn支持非线性资源共享，并证明类型保持、无死锁与弱规范化。
在 C11 中实现并验证 release-acquire 事务内存
提出松弛操作语义 TMS2-ra，与 RC11 集成，给出验证逻辑 TARO 和 C11 实现 TML-ra，并在 Isabelle/HOL 中验证。
共享与变异的余效应
提出用余效应跟踪命令式程序中的变量共享，并扩展类型系统以简洁建模唯一性与不可变性。
面向多执行内存模型的模型检测
提出强化多执行内存模型 Weakestmo2，并实现性能接近逐执行模型工具的模型检测器 WMC。
为 DOT 辩护：具有模式匹配和 GADT 风格推理的对象的理论基础
提出 cDOT 演算，为对象语言中的子类型重建提供形式基础，并将 GADT 风格推理编码进来。
Go 泛型到 Go：字典传递、单态化与混合方法
提出基于调用点的字典传递泛型翻译并证明正确性，以克服 Go 1.18 混合方案的限制。
在 Coq 中将规范 SQL 翻译为命令式代码
在 Coq 中机械化验证了从规范 SQL 查询到命令式代码的编译器 DBCert，覆盖相关查询与 NULL 语义。
在线数据处理的本质
提出 DON 演算，首个在线数据处理的形式基础，以操作流统一增量处理与时间局部性优化，并机械化证明可观察等价。
使用逻辑学习合成公理化
提出用逻辑学习与合成技术自动发现结构类的公理化，并在部分情形自动证明完备性。
领域特定语言的组合式嵌入
提出组合式嵌入，在 CP 语言中兼得浅层与深层嵌入优势，支持 DSL 语言复用、模式匹配与可扩展解释。
安全对象初始化的概念框架：Celsius 模型的原则化与机器化可靠性证明
提出安全对象初始化的四条核心原则，并以最小演算 Celsius 及 Coq 机器化证明实现兼具表达力与简洁性的初始化系统。
组合式虚拟时间线：验证具有算法时间隔离的动态优先级分区
提出组合式虚拟时间线抽象，用 Coq 机器化验证带预算的 EDF 分区内核并证明分区间时间隔离。
依赖分析的 monadic 与 comonadic 方面
本文用范畴论中 monadic 与 comonadic 思想设计统一依赖分析演算，涵盖并解释 DCC 与 λ∘。
Veracity：利用可交换性的声明式多核编程
提出声明式多核编程范式，程序员以顺序方式书写并显式标注代码片段的可交换条件，编译器据此自动并行化。
UniRec：一个用于嵌套递归与循环的类幺模框架
提出 UniRec，一个统一嵌套递归与完美嵌套循环调度变换、并推广幺模框架的类幺模框架。
分布式可重构系统的推理
提出基于分离逻辑与归纳谓词的 Hoare 风格演算，用 havoc 不变式验证可重构分布式系统。
面向 WebAssembly 的快速原地解释器
提出无需改写、无需独立内部格式的 WebAssembly 原地解释器，性能媲美解释定制格式。
Tower：量子叠加中的数据结构
提出 Core Tower/Tower 量子编程语言与 Boson 分配器，实现可逆、历史无关、有界时间的量子叠加数据结构。
樱桃时节：在能力机器上使用定向能力实现高效的时间栈安全
提出定向能力使能力机器调用约定更高效，并用一元/二元逻辑关系与编译器完全抽象证明时间栈安全性，Coq机械化。
减少浏览器内存使用的最优堆上限
提出无需通信即可在多堆间最优分配内存的平方根堆上限规则，并在 V8 中显著降低内存或 GC 时间。
并发 size 操作
提出为并发集合与字典添加线性一致、wait-free 的 size 操作的方法，性能开销低。
SigVM：为真正去中心化的智能合约启用事件驱动执行
提出首个扩展 EVM 支持事件驱动执行的区块链虚拟机，通过信号事件实现合约间自动触发，消除对中心化链下中继的依赖。
引导式分解能帮助终端用户编写更大的块基程序吗？一项移动机器人实验
提出引导式程序分解的块编程系统，用户实验表明它显著提升终端用户应对大规模任务的成功率。