ICSE 2291 ASE 2141 FSE 1566 ASPLOS 1219 LMCS 1020 OOPSLA 737 LICS 679 ISSTA 617 POPL 609 ICFP 374 PLDI 369 TOPLAS 199 JFP 172 arXiv 预印本 5
标签：程序验证（共 1033 篇，按优先级展示前 200）
LLM 遇上界模型检测：神经符号循环不变式推断
提出“查询-过滤-重组”策略，用 LLM 生成候选循环不变式、以有界模型检测筛选谓词并组装，再由 SMT 求解器校验。
无循环展开的有界模型检测中由LLM生成的循环不变式
用LLM生成循环不变式并由一阶定理证明器校验，从而在CFG层面消除循环，扩展有界模型检测对无界循环程序的验证能力。
AutoVerus：为 Rust 代码自动生成证明
提出 AutoVerus，用 LLM 智能体网络自动为 Rust 代码生成 Verus 正确性证明，90%+ 任务成功。
KVerus：面向 Rust 代码的可扩展且鲁棒的形式化验证证明生成
提出 LLM 辅助的 Verus 证明生成工作流 KVerus，用动态知识库支持仓库级跨文件证明生成与修复。
智能体程序验证中的自动化引理发现
提出 LLM 智能体 LemmaNet，通过程序语义理解离线合成与在线适配辅助引理，自动完成演绎验证中的 VC 证明。
Fun2spec：大规模代码契约合成
首个工业级工具，引导 LLM 合成带量词的一阶逻辑 C++ 规范，准确率达 85%。
通过对局部推理错误的反馈引导基于 LLM 的循环不变式合成
通过形式化验证 LLM 的推理步骤并定位局部逻辑错误，为其循环不变式合成提供建设性反馈，显著提升成功率。
SpecGen：基于大语言模型的形式化程序规约自动生成
SpecGen 利用 LLM 对话式生成并变异筛选可验证的形式化程序规约，在 385 个程序上成功生成 279 个可验证规约。
HoarePrompt：面向自然语言中程序正确性的结构化推理
提出 HoarePrompt，将最强后置条件与 k-归纳引入 LLM，用自然语言推理程序对需求的正确性。
Laurel：用大语言模型解除自动验证的阻塞
Laurel 利用大语言模型自动生成 Dafny 断言，通过错误定位与代码库示例提示，减少验证器所需人工提示。
贝叶斯分离逻辑：概率编程的逻辑基础与公理语义
提出贝叶斯分离逻辑 BaSL，为贝叶斯概率编程提供逻辑基础与公理语义，并支持贝叶斯更新等模块化推理。
LLM 辅助的高保障 C 程序合成
提出 SynVer，用两个 LLM 分别合成 C 程序候选并生成 Rocq/VST 正确性证明，实现高保障 C 程序合成。
SpecPylot：基于大语言模型的 Python 规约生成
提出 SpecPylot，用 LLM 生成 icontract 规约，并借助 CrossHair 符号执行验证与反例驱动迭代修正。
面向 Move 程序的智能体式规约生成器
提出 Msg，面向 Move 智能合约自动生成可验证规约，84% 函数成功，可验证子句提升 57%。
带天使式假设的开放程序内存安全验证
提出 Seeker，用 LLM 挖掘惯用模式并实例化为天使式假设来补全缺失代码，以高精度区分开放程序内存安全误报与真实缺陷。
仅凭测试能否合成形式规约？
用 LLM 仅从测试代码与动态执行轨迹（黑盒）推断 JML 形式规约，并以有界模型检验迭代精化。
利用系统级观测为定量验证中的模型参数贝叶斯学习提供信息
提出 EPIK，用可直接观测的系统级属性引导贝叶斯先验，从而更准确地对模型转移参数学习并验证难以测量的定量性质。
HarnessLLM：用大语言模型生成 Rust 验证 harness
提出 HarnessLLM，从既有测试套件自动抽取调用场景并用 LLM 增量生成、迭代修复 Rust 验证 harness，检出 6 个真实内存安全缺陷。
驯服 GPU 内核中 Tensor Core 的位级行为：黑盒重建、编译器强制与静态验证
刻画 GPU 归约与 GEMM 的位级决定因素，实现闭源库算术的黑盒重建、Triton 归约顺序强制与位等价静态验证。
1001 行代码的故事：潜在运行时错误引导的规约合成用于验证大规模程序
提出 Preguss，以潜在运行时错误引导静态分析与 LLM 分治合成过程间规约，实现千行级程序的高自动验证。
TensorRight：张量图重写的自动验证
提出首个可验证任意秩与尺寸张量图重写正确性的自动验证系统 TensorRight。
LLM 辅助的安全协议验证自动建模
提出用 LLM 分阶段自动从自然语言文档生成安全协议的符号模型，并用可证可靠的模型变换保证正确性。
从深度学习模型中推断数据前置条件以实现部署中的可信预测
提出 DeepInfer：将训练好的 DNN 抽象为可做最弱前置条件推理的表示，从输出后置条件推断输入前置条件，以判定部署预测的可信性。
PAT-Agent：面向模型检测的自动形式化
提出 PAT-Agent，结合 LLM 规划、代码生成、PAT 模型检测与反例修复，实现自然语言到可验证形式模型的端到端自动形式化。
ML GPU 内核的等价性检查
提出首个 GPU 内核等价性检查器，形式化验证手工、LLM 与编译器优化的 ML 内核正确性。
保证浮点神经网络分类一致性的量化
提出CoMPAQt用MILP验证量化网络分类不一致性，并给出保证或近似保证与浮点网络分类一致的纠正机制。
It Takes Two to Entangle：分布式机器学习模型的细化检查
提出 Entangle，用迭代重写静态检查分布式模型是否细化顺序模型，以定位分布式 ML 中的 bug。
面向需求驱动代码验证的AI多智能体系统及其工业部署
提出并工业部署ARC-V多智能体系统，用LLM实现需求驱动的代码验证与早期缺陷发现。
Spec2Code：将协议规范映射到函数级代码实现
提出首个LLM驱动的函数级协议规范到代码映射框架，支持细粒度一致性检查并发现真实不一致。
不正确性逻辑
提出与 Hoare 正确性逻辑对偶的“不正确性逻辑”，用于形式化程序错误与缺陷推理。
ESBMC 5.0：一个工业级 C 模型检测器
推出工业级开源 C 模型检测器 ESBMC 5.0，新增前后端、IEEE 浮点支持与改进的 k-归纳算法。
用不正确性逻辑在大程序中发现真实 bug
基于不正确性逻辑与分离逻辑的融合 ISL 实现自动分析器 Pulse-X，在 OpenSSL 中发现 15 个真实内存错误。
Fairify：神经网络的公平性验证
提出基于 SMT 的神经网络个体公平性验证方法，通过输入划分与神经元剪枝实现可扩展的认证与反例生成。
ReluDiff：面向相关神经网络的差分验证
提出 ReluDiff，对两个相关神经网络进行差分形式验证，通过前向区间分析与反向梯度精化证明输出差异性质，显著加速验证。
定量分离逻辑：一种推理概率指针程序的逻辑
提出定量分离逻辑 QSL，为概率指针程序提供带局部推理的定量最弱前置条件演算。
高阶概率程序的形式验证：关于近似、收敛、贝叶斯推断与优化的推理
提出 PPV 逻辑族，用于验证带连续分布和高阶函数概率程序的近似、收敛、贝叶斯推断与优化性质。
面向 DNN 的基于 PAC 模型学习的实用鲁棒性分析
提出基于 PAC 模型学习的黑盒框架，将模型学习融入 DNN 局部鲁棒性分析，提升实用性与可扩展性。
NeuroDiff：面向前馈 ReLU 神经网络差分验证的符号化细粒度近似
提出 NeuroDiff，用新凸近似与符号变量细粒度界定两个 ReLU 网络输出差，实现高精度快速差分验证。
面向循环不变式学习的区间反例
提出区间反例以提升循环不变式黑盒学习中的样例质量，减少约束查询次数。
面向 ML 赋能系统安全的感知契约
提出感知契约，用于刻画神经感知误差并保障基于视觉感知的控制系统安全。
面向 Sigmoid 类神经网络鲁棒性验证的可证明最紧线性近似
提出网络级紧致性统一定义，并设计两种可证明最紧的线性近似，显著提升 Sigmoid 类网络鲁棒性验证精度。
神经网络全局鲁棒性的验证
提出面向分类器的全局鲁棒性性质与 anytime 验证器 VHAGaR，计算最小全局鲁棒界并显著优于已有验证器。
面向软件验证算法选择的注意力与表示
提出 Attend and Represent，用注意力与表示学习改进软件验证算法选择，并关注可解释性。
基于 GNN 的作业调度器的可扩展验证
提出 vegas，首个可扩展验证基于 GNN 的作业调度器单步与多步性质的形式化框架。
面向少像素攻击的深度学习鲁棒性验证
提出 Calzone，首个对 L0（少像素）对抗攻击给出可靠且完备分析的神经网络鲁棒性验证器。
具有可证明保证的深度学习安全性与鲁棒性
提出面向深度神经网络的自动验证与测试技术，对有界输入扰动给出可达输出集的上下界，并提供可证明保证。
C 语言的健全静态数据竞争验证：这场竞争输了吗？
通过真实程序基准与代码惯用法微基准，揭示健全静态数据竞争验证工具的能力、局限与不健全性。
Prophecy：从神经元激活推断形式化性质
提出工具 Prophecy，通过神经元激活状态自动推断神经网络的形式化性质，支持解释、验证与监控。
MINES：通过 Web API 不变式推断实现可解释异常检测
从 API schema 推断可解释不变式，用正常日志筛选后生成 Python 代码检测 Web 异常，显著优于日志学习基线。
EMERGE：通过规则合成检查 LLM 的实现等价性
提出 EMERGE，借助规则合成检查 LLM 的实现等价性，并发布 ASE 2026 工件。
揭示大语言模型在依据自然语言规约验证代码时的系统性失败
发现并分析 LLM 判断代码是否满足自然语言规约时存在系统性误判，并提出缓解提示策略。
VERT：基于大语言模型的多语言可验证等价 Rust 转译
结合大语言模型与模型检测，将任意可编译到 WebAssembly 的语言转译为等价且地道的 Rust。
为深度神经网络合成 Boxes 前置条件
提出 PreBoxes 框架，用猜测-检验自动合成 DNN 的 Boxes 充分前置条件，并支持迭代求解更弱条件。
基于 LLM 与概率模型检测的网格世界路径规划
提出 LLM 与概率模型检测结合的神经符号路径规划框架，为随机网格世界提供时序与概率保证。
投影式解码：迈向语义感知的 LLM 生成
提出投影式解码，在生成中同步维护部分图模型，以可证明方式引导 LLM 产出语义有效结果。
探究形式化验证在软件开发中的作用：从自动规约生成到验证语言的可用性
通过实证研究考察形式化注释对代码理解的影响、LLM自动生成规约及验证工具可用性，以提升形式化验证的实用性。
持续推理
提出持续推理，将形式化推理融入持续迭代的代码库开发，以扩展形式化方法的适用范围。
深度神经网络的可扩展定量验证
提出面向 DNN 的可扩展定量验证框架 PROVERO，用测试驱动方式证明概率性质，并可验证大规模网络的鲁棒性。
PRIMA：通过可扩展凸包近似实现通用且精确的神经网络认证
提出 PRIMA，用可扩展凸包近似实现通用且精确的神经网络形式认证。
低目标更难：概率程序验证中用于下界的归纳法
提出无需序列极限、仅需有限次应用循环体语义的概率程序期望值与运行时间下界归纳验证规则。
Outcome Logic：正确性与不正确性推理的统一基础
提出 Outcome Logic，统一正确性与不正确性推理，并证明错误规约可在其自身中证伪。
如果人类能看见，你的系统也应该能看见
提出以人类性能为基线的机器视觉组件可靠性需求，并自动检查模型是否满足。
面向符号执行的分段内存模型
提出分段内存模型，缓解符号执行处理复杂堆结构时因指针可指向多个对象而大量分叉的问题。
Lilac：一种面向条件概率的模态分离逻辑
提出 Lilac 分离逻辑，以分离合取刻画概率独立性，并基于 disintegration theory 引入条件概率模态。
QVIP：一种基于ILP的量化神经网络形式化验证方法
首次将量化神经网络验证编码为整数线性约束，提出可靠且完备的QVIP方法，性能显著优于现有方法。
几乎正确的不变式：通过对证明进行模糊测试来合成归纳不变式
提出 Achar，用主动学习提出候选不变式，并以模糊测试反证之，从而为含不可解释操作的开放程序合成归纳不变式。
PRODeep：深度神经网络鲁棒性验证平台
提出 PRODeep 平台，集成约束、抽象与优化三类算法，支持深度神经网络鲁棒性验证与算法组合。
使用机器学习挖掘软件组件的环境假设
提出 EPIcuRus，结合搜索测试、决策树学习与模型检测，自动为软件组件合成环境假设。
Fuzzi：一种面向差分隐私的三层逻辑
提出面向差分隐私的三层逻辑 Fuzzi，打通敏感度类型逻辑与 apRHL，实现自动且灵活的隐私验证。
BlueBell：关系提升与独立性的联盟及其在概率推理中的应用
提出概率程序逻辑 BlueBell，以“联合条件化”模态统一一元式与关系式概率推理。
一种面向条件独立性的束逻辑
扩展 BI 逻辑以非交换合取刻画条件独立，并基于 Markov 核与幂集单子给出模型和概率程序验证逻辑。
为符号执行合成求解策略
将符号执行划分为两阶段，用第一阶段公式在线合成SMT求解策略以提升后续约束求解效率。
深度神经网络（DNN）的架构保持可证明修复
提出架构保持的 V-polytope 可证明修复方法，仅改参数即可让 DNN 在指定凸多面体上满足规格，并实现工具 APRNN。
证明具有随机化、依赖于变量的终止时间的概率程序的期望敏感性
提出基于鞅的可靠方法，证明迭代次数随机依赖输入的概率 while 循环的期望敏感性，并可自动化与组合。
Halide 语言的端到端翻译验证
提出 Halide 端到端翻译验证算法，用 prophetic 注解和 refinement 映射证明生成代码正确。
正几乎必然终止：复杂度与证明规则
证明概率程序的PAST复杂度为Π^1_1完全，并给出基于超限序数的可靠完备证明规则。
大规模非终止性证明
提出组合式欠近似非终止证明逻辑 UNTer_SL，并实现可扩展分析器 Pulse∞，在数十万行代码库中发现未知非终止缺陷。
学习合成关系不变式
用 SyGuS 生成候选、SMT 验证器过滤，并借助逻辑推理剪枝与强化学习排序，高效合成关系不变式。
数据驱动的循环界学习用于终止性分析
提出数据驱动的循环界学习方法，结合学习器与验证检查器，高效证明程序终止性。
基于神经网络的定量验证
用神经网络表示上鞅证书，通过反例引导的归纳合成循环，为概率程序与随机模型计算紧致且可靠的概率界。
SATune：一种面向可配置软件验证工具的实证研究驱动自动调优方法
通过实证数据集揭示验证工具无通用最优配置，并提出基于代理适应度搜索的自动配置工具 SATune。
Fairquant：深度神经网络公平性的认证与量化
用抽象与公平性引导的迭代精化，对深度神经网络进行个体公平性的形式化认证，并能量化可证明公平个体的比例。
ReLU 凸包近似
提出快速精确的 ReLU 凸包过近似方法 WraLU，用更少约束实现更紧近似并集成到神经网络验证器 PRIMA。
强不变式很难：论（概率）程序最强多项式不变式的困难性
证明单路径多项式循环的最强多项式不变式计算至少与 Skolem 问题同难，并推广到概率程序的矩不变式。
深度神经网络的属性推断
提出自动推断前馈神经网络形式化属性的技术，从神经元激活模式中提取蕴含期望输出性质的输入与层属性。
两种近似的故事：通过下近似收紧 DNN 鲁棒性验证中的过近似
提出双重近似方法，利用激活函数的下近似域收紧线性过近似，提升 DNN 鲁棒性验证的紧致度与可扩展性。
概率编程的确定性流采样：语义与验证
提出以采样器为中心的高阶概率语言，给出操作/指称语义，并建立验证采样器正确性的演算。
MutDafny：一种基于变异的 Dafny 规约评估方法
提出 MutDafny 工具，用 40 个变异算子通过变异测试自动暴露 Dafny 形式规约的弱点。
云规模授权的形式化验证
用 Dafny 重写并形式化验证 AWS 授权引擎，保持行为兼容并成功部署，性能提升三倍。
MLIR 的一等验证方言
将形式语义作为一等公民引入 MLIR，设计验证方言以支持编译器 IR 的语义编码与通用验证工具。
利用自动条件独立性推理实现因果发现算法的运行时验证
提出通过自动条件独立性推理对因果发现算法进行运行时验证的方法。
定量符号相似性分析
提出对语义非等价性进行定量推理的符号相似性分析，可定位程序等价与不等价的具体输入区间。
量化神经网络中比特翻转攻击的验证
提出首个针对量化神经网络比特翻转攻击的形式化验证框架，可证明其免疫或定位所有脆弱参数。
DNN 认证器健全性的自动验证
提出 ProveSound，通过符号化 DNN 将 DNN 认证器的健全性验证归约为 SMT 可处理问题，实现任意架构认证器的自动验证。
反例潜力引导的神经网络高效增量验证
提出基于反例潜力的增量神经网络验证方法 Olive，优先重验更可能含反例的子问题以尽早发现反例。
CXLMC：CXL 共享内存程序的模型检测
提出 CXLMC，对 x86-CXL 共享内存程序的崩溃执行进行模型检测，在 8 个应用中发现 24 个缺陷。
面向深度神经网络性质修复的补丁合成
提出 Patchpro，通过构造补丁模块并结合形式验证，实现对 DNN 局部鲁棒性的可证明性质级修复。
面向神经网络回归的认证持续学习
提出认证持续学习，在再训练神经网络时尽可能保持已认证的正确性，并兼顾效用。
MpBP：利用多路径界传播验证神经网络的鲁棒性
提出 MpBP，通过多路径扩展经典界传播，高效验证神经网络鲁棒性。
基于最大路径因果性的并发验证
提出最大路径因果性模型，把到达同一路径的调度与输入组合归为等价类，统一探索并发程序调度与输入空间。
连续概率程序演绎验证的基础：从勒贝格到黎曼再返回
提出用黎曼和近似积分，将连续概率程序的期望界验证归约为 SMT 不变量验证，并证明收敛与 coRE 完全性。
通过关系界传播实现可扩展的关系分析
提出关系界传播方法，通过语义规则自动收紧关系逻辑公式的界，提升有界模型检查的可扩展性。
RustAssure：面向 LLM 转译 C-to-Rust 代码的差分符号测试
用 LLM 将 C 代码转译为 Rust，并通过差分符号测试验证转译结果与原代码的语义等价性。
通过使神经元失稳生成具有挑战性的神经网络验证基准
提出 ReluSplitter，通过语义保持地使稳定神经元失稳，自动生成难度可调且真值可验证的 DNN 验证基准。
神经网络终止性分析
用神经网络表示 ranking function，并经符号验证为程序提供终止性证书。
通过 iDP 验证守护神经网络分类器的仅标签访问隐私
LUCID 用形式化验证计算 iDP 确定性界，只对不满足 iDP 的标签加噪，以极小精度损失守护标签访问隐私。
LLVM AArch64 后端的翻译验证
提出 arm-tv，形式化验证 LLVM IR 到 AArch64 汇编的翻译，并在该后端发现 45 个此前未知的误编译缺陷。
为翻译验证建模局部内存的动态分配与释放
提出局部内存动态分配的执行模型与精化定义，将编译器翻译验证可靠地归约为 SMT 可解的一阶逻辑查询。
分离逻辑的系统化设计
提出从程序语义系统推导内嵌局部性原理的局部公理与框架规则的方法。
未修改系统软件安全属性的高度自动化验证
提出 Spoq2，首个高度自动化验证未修改系统软件安全属性的框架，通过降低验证复杂度使 SMT 求解可行。
深度神经网络的可证明公平性修复
提出 PROF 框架，利用区间界传播与 MILP 求解，为 DNN 公平性修复提供可证明保证并提升泛化。
面向张量运算的基于搜索的翻译
提出用程序合成与验证自动把通用语言程序翻译为语义等价的张量运算，替代传统模式匹配。
使用梯度下降学习 DNN 抽象
提出用连续参数表示 DNN 抽象构造，并用梯度下降搜索抽象空间，避免 CEGAR 陷入次优抽象。
神经网络的定量鲁棒性分析
聚焦神经网络定量鲁棒性验证，旨在不仅判定邻域内是否存在误分类输入，还度量其比例并构建系列工具。
从需求推断性质并自动化其形式验证
提出用 SML 元模型表达示例数据，并改进 ILP 自动推断性质，以降低形式验证中规约与证明的人工交互。
从对称样本学习对称不变式
提出对称决策树SDT及Horn-SDT方法，从对称样本学习对称不变式，加速参数化程序验证。
SART：神经网络验证中二元变量约简的符号-绝对值重构理论
提出 SART 理论，打破不稳定 ReLU 神经元与二元变量的一一对应，从编码源头降低神经网络完备验证的复杂度。
可解元组模式及其在程序验证中的应用
提出可从少量正样本高效推断的（合取）可解元组模式，并用于 CHC 求解器验证递归数据结构程序。
支撑三角形机器（Support Triangle Machine）
提出凸近似提升问题及支撑三角形机器，将单神经元近似提升为更精确的多神经元近似，用于DNN验证。
用于验证 eBPF 程序的流敏感精化类型系统
提出流敏感精化类型系统，在用户态自动推断 eBPF 验证证明证书，缩小可信基并提升可调试性。
概率程序的结构抽象与精化
提出结构抽象精化框架，将概率控制流自动机抽象为MDP，并用CEGAR复用非概率验证技术验证概率程序阈值问题。
匹配逻辑
提出匹配逻辑，一种以模式与模式匹配统一刻画结构和推理的一阶逻辑变体，可泛化多种程序分析逻辑并支持 SMT 求解。
RustHorn：基于 CHC 的 Rust 程序验证
提出将带指针与动态内存的 Rust 程序归约为 CHC 的新方法，利用权限保证消除指针和内存状态，并证明可靠性与完备性。
快速、可靠且有效完备的动态数据竞争预测
提出多项式时间且无假阳性的动态数据竞争预测算法 M²，对两进程完备并可动态判定完备性。
VeriAbs：通过抽象与测试生成进行验证
提出 VeriAbs，一个面向 C 程序的可达性验证器，按循环类型选择由抽象、模型检测与测试生成等技术组成的策略组合。
C2S：将自然语言注释翻译为形式化程序规约
提出 C2S，通过从已有注释与规约中学习词-token 对齐，将自然语言注释自动翻译为形式化程序规约。
概率分离逻辑
提出概率分离逻辑 PSL，用分离建模概率独立，并验证密码构造的信息论安全性。
概率程序的相对完备验证：一种用于基于期望推理的表达性语言
提出一种表达力充分的定量断言语法，使概率程序基于期望的验证系统达到相对完备。
Google Native Client 的健全循环超优化
提出健全的循环超优化架构，用完全健全验证与有界验证指导搜索，显著提升 NaCl libc 性能。
混合符号期望的最弱前置期望语义
提出可处理混合符号无界随机变量期望的概率程序最弱前置期望演算，保证语义总良定义且可靠。
概率终止的可靠且完备证明规则
为带离散概率选择与有界恶魔非确定性的命令式程序，给出算术断言语言中可靠且相对完备的定性/定量概率终止证明规则。
通过 SMT 求解增强的强化学习推断循环不变式
提出 RL 剪枝与 SMT 求解协同的框架，在一般非线性假设空间中高效推断循环不变式。
面向自动驾驶系统的基于仿真的验证方法
结合工业仿真器与形式化测试环境，系统化生成高风险场景并用一阶线性时序逻辑在运行时监控属性。
非确定性自动机的高效约简及其在语言包含测试中的应用
提出高效的 NFA/NBA 约简算法，并显著扩展语言包含等 PSPACE 完全问题的可解规模。
归约 DNN 性质以支持对抗攻击的证伪
提出保语义归约，将多类 DNN 安全性质统一转化为可用对抗攻击求解的等价正确性问题。
JaVerT 2.0：面向 JavaScript 的组合式符号执行
提出统一的组合式符号执行方法，构建 JaVerT 2.0，首次为 JavaScript 支持基于双向溯因的自动组合测试。
通过高层调度重写实现经验证的张量程序优化
在 Coq 中构建轻量框架，用一系列经验证的语义保持重写，对纯函数式数组语言写的张量核进行调度优化。
并发不正确性分离逻辑
将不正确性分离逻辑扩展到并发程序，提供参数化框架检测竞态、死锁和内存安全错误并保证真阳性。
概率敏感性的前期望演算
提出关系前期望演算，用Kantorovich距离上界约束概率程序两次执行输出的分布距离。
论核心：马尔可夫决策过程的部分探索框架
提出 MDP 部分探索框架，通过识别高概率核心并给出严格误差界，高效近似分析多种时域性质。
高阶分离逻辑中的异步概率耦合
提出支持异步概率耦合的高阶概率关系分离逻辑 Clutch，并用于证明高阶程序的上下文精化与等价。
错误信用：面向高阶概率程序错误界的有资源推理
提出 Eris 高阶分离逻辑与错误信用，证明高阶概率程序的精确错误概率上界。
CN：用分离逻辑精化类型验证系统 C 代码
设计并实现 CN——面向系统 C 代码的分离逻辑精化类型系统，并验证 pKVM 组件。
Minotaur：面向 SIMD 的合成超优化器
用程序合成与形式验证为 LLVM 搜索整数/浮点 SIMD 优化，获得实际加速。
基于时序不变量的模块化控制平面验证
提出 Timepiece，用逻辑时间路由模型与受时序逻辑启发的接口谓词，实现可靠可扩展的模块化控制平面验证。
面向概率程序的演绎验证基础设施
提出首个面向概率程序的演绎验证基础设施，用实值逻辑、中间验证语言与最弱前置条件支持期望型性质的自动验证。
通过符号不变式差异理解自动生成的补丁
利用形式不变式集合的差异与蕴含距离刻画自动生成补丁的语义相似性，并聚类以减轻人工审查负担。
PerSeVerE：ext4 下用于验证的持久性语义
形式化 ext4 与 C/C++ 弱内存的持久性语义，提出模型检测验证方法并发现编辑器缺陷。
V8 JavaScript 引擎中 JIT 编译器的翻译验证
提出 TurboTV：基于 SMT 的分阶段翻译验证器，验证 V8 TurboFan JIT 编译的正确性并发现 LLVM 新误编译。
神经网络的增量验证
提出增量且完备的 DNN 验证框架与工具 IVAN，避免网络更新后从头验证并显著加速。
控制流引导的 SMT 求解用于程序验证
提出在 SMT 求解中利用程序控制流知识剪枝搜索空间，显著提升程序验证效率。
加权编程：一种用于规约数学模型的编程范式
提出加权编程范式及 Dijkstra 风格的 wp/wlp 演算，用以规约并推理超出概率分布的数学模型。
一种用于负相关性的分离逻辑
提出概率分离逻辑 LINA，用两种分离合取分别刻画独立性与负相关性，并验证哈希数据结构等随机程序。
ICEBAR：面向 Alloy 规约的反馈驱动迭代修复
提出 ICEBAR，以 Alloy 规约中固有的断言与谓词作为性质型 oracle，迭代修复规约并缓解过拟合。
基于惰性顺序化的多线程程序有界验证
提出惰性顺序化，将有界多线程 C 程序转为串行程序，复用 BMC 高效验证并发。
一种定量概率关系霍尔逻辑
提出定量概率关系霍尔逻辑 eRHL，克服 pRHL/apRHL 的随机对齐限制，并给出可靠性与完备性结果。
基于 Farkas 引理的可扩展线性不变式生成
提出两项改进，显著提升基于 Farkas 引理的仿射程序线性不变式生成的扩展性。
CUDA 内核求值代价的建模与分析
提出面向 CUDA 内核的定量程序逻辑与代价语义，可自动推导符号化资源上界并检测性能瓶颈。
面向符号执行的类型与区间感知数组约束求解
提出类型与区间感知公理生成及ILP预检，加速符号执行中的数组约束求解。
结果逻辑中的概率并发推理：独立性、条件化与不变式
提出 pcOL，首个能表达概率并发程序完整结果分布的程序逻辑，并支持几乎必然终止等推理。
可能发散的概率程序的下界
提出不依赖几乎必然终止的新证明规则，为可能发散的概率程序建立终止概率与期望值的非平凡下界。
面向运行时概率模型检验的区间变化点检测
提出高效区间变点检测并与贝叶斯估计器集成，使运行时概率模型检验能应对参数突变。
CPA-SymExec：CPAchecker 中的高效符号执行
在 CPAchecker 中实现基于抽象与 CEGAR 的符号执行，自动识别符号事实以缓解路径爆炸并判定可达性。
使用 Kripke 规约单子的经过验证的符号执行（且无需元编程）
提出基于 Kripke 规约单子构造符号执行验证器并证明其可靠性的系统方法，在 Katamaran 中全验证实现。
H-Houdini：可扩展的不变式学习
提出 H-Houdini，用可并行、可记忆化的分层增量 SMT 检查替代整体式检查，使归纳不变式学习扩展到大型硬件设计。
可解多项式理想：程序分析中的理想反射
将任意循环抽象为可解多项式映射模型，从而把循环多项式不变式生成技术推广到一般程序。
面向已验证库的半自动化证明修复
提出首个高阶命令式函数的证明修复方法，在 Coq 中结合动态对齐和不变量综合，自动生成大部分证明并留下少量残余义务。
面向带最小不动点一阶逻辑的模型引导归纳引理合成
提出用有限一阶模型作为反例引导，合成带最小不动点一阶逻辑中的归纳引理以证明公式有效性。
CSim²：Isabelle/HOL 中基于 rely-guarantee 的并发系统组合式自顶向下验证框架
在 Isabelle/HOL 中提出组合式 rely-guarantee 仿真框架 CSim²，将并发系统高层规约的性质自顶向下保持到实现层。
高阶概率对抗计算：范畴语义与程序逻辑
为高阶概率对抗计算建立一元与关系程序逻辑，并在准 Borel 空间范畴中证明可靠性。
面向 SC、TSO 和 PSO 内存模型的模序一致性理论可满足性
提出适用于 SC、TSO 和 PSO 内存模型的序一致性理论及 SMT 求解器 Zord，显著提升并发程序验证性能。
判定差分隐私方案的准确性
提出基于程序不连续性的通用准确性定义，并研究差分隐私方案准确性判定的可判定性与判定过程。
内联汇编的接口合规性：自动检查、补丁与精化
提出首个自动形式化检查 GNU 内联汇编接口合规性的技术 RUSTInA，并能为部分问题生成经过证明的补丁与精化。
SpaceSearch：用于构建和验证求解器辅助工具的库
提出 Coq 库 SpaceSearch，让用户在证明助手中构建并验证求解器辅助工具，再提取到 Rosette 高效执行。
迈向 GPU 一致性模型的统一分析
将 PTX 与 Vulkan 一致性模型集成到 Dartagnan，实现首个可分析真实 GPU 代码的多模型验证工具，并发现原模型两处缺陷。
有根基的多模态程序验证器
提出基于 Lean 的框架，用 monad transformer 代数自动导出可靠的验证条件生成器，以构建有根基的多模态程序验证器。
面向运算符优先级语言的模型检测器
提出并实现了首个开源模型检测器 POMC，用于验证运算符优先级语言程序上的 POTL 树结构性质。
当少即是多：弱算术理论中的后承发现
提出弱公理化乘法的非线性算术理论及后承发现算法，用于生成循环不变式并证明程序安全性质。
面向自动程序验证的 HFL(Z) 有效性检查
提出 HFL(Z) 公式有效性的自动判定方法，配合归约实现对高阶函数式程序各类时序性质的统一全自动验证。
通过网络约简加速神经网络验证
提出网络约简预处理方法，消除稳定 ReLU 神经元并将网络转为顺序结构，从而加速现有神经网络验证工具。
JSTAR：使用精化的 JavaScript 规范类型分析器
首个对 ECMAScript 规范做类型分析并检测规范缺陷的工具，借助基于条件的精化提升分析精度。
基于操作博弈语义的组合式关系推理
提出 Kripke 范式双模拟，用操作博弈语义统一四类高阶语言的上下文等价关系推理，并证明其可靠完备。
上鞅、秩函数与概率 λ 演算
提出基于秩上鞅的概率λ演算几乎必然终止证明方法，并给出反单调、稀疏与替代归约策略下的扩展。
一种分析 Alloy 规范的演化方法
提出 EvoAlloy，将遗传算法引入 Alloy，在保持可靠性的前提下放宽完备性，以扩展可处理规范规模。
基于依赖细化类型系统的高阶概率程序自动验证
提出依赖细化类型系统，将高阶概率程序的多种定量性质验证归约到扩展 CHC 求解，并可复用现有求解器。
VMSL：面向通过 FF-A 通信的虚拟机机械化鲁棒安全性的分离逻辑
提出分离逻辑 VMSL，可模块化推理 FF-A hypercall ABI 上通信的虚拟机并机械化证明其鲁棒安全性。
揭秘面向位向量程序的基于模板的不变式生成
系统实验揭示位向量程序中模板不变式生成的模板与求解器影响，并证明其可处理现有方法难处理的基准。
LIV：使用直线程序进行循环不变式验证
提出 LIV 工具，将循环不变式验证拆分为无循环直线程序上的验证任务，从而更实用地检查不变式是否足以构成归纳安全证明。
基于符号执行的可靠渐进验证
为基于符号执行的渐进验证给出形式化与可靠性证明，并发现修复实现中的可靠性缺陷。
概率程序的等价性与相似性反驳
提出首个全自动、可处理无限状态、带形式保证的概率程序等价性与相似性反驳方法
使用符号执行发现 ∀∃ 超属性缺陷
提出扩展符号执行以支持迹量化的全自动方法，用于发现 ∀∃ 超属性的违反。
vCXLGen：面向异构架构的 CXL 桥自动合成与验证
提出 CXL 桥抽象并实现 vCXLGen，可从机器可读的一致性协议规范自动合成并组合验证异构 CXL 桥。
ESBMC-Python：面向 Python 程序的有界模型检测器
提出首个基于有界模型检测的 Python 程序验证工具，借助类型标注与 SMT 求解器实现自动化验证。
视角博弈（Perspective Games）
提出视角博弈模型，其中玩家仅观察自己拥有的顶点，并研究其获胜策略判定、ATL*模型检测及策略表达能力。
CF-GKAT：控制流变换的高效验证
提出 CF-GKAT，扩展 GKAT 以支持非局部控制流和硬编码值，高效可靠完备地验证控制流变换的迹等价。
反例驱动的量词实例化及其在分布式协议中的应用
提出反例驱动的关系抽象与细化方法，避免量词实例化导致SMT求解器发散，并验证共识协议安全性质。
性质导向可达性作为单调理论中的抽象解释
将命题PDR重构为单调理论中的抽象解释，并用最佳变换器刻画其不变式推断。
学习归纳不变式的边界
将精确概念学习理论引入不变式推断，提出 fence 条件，首次给出插值式不变式推断的多项式复杂度结果。
单元证明有效吗？面向内存安全验证的组合有界模型检验的实证研究
首个内存安全验证中单元证明的实证研究，提出系统化构建方法并评估其效果与成本。
验证金融科技系统中的数据约束等价性
提出 EQDAC，一种高效判定数据约束等价性的决策过程，用于检测金融科技系统中的冗余约束。