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
标签：定理证明与证明工程（共 627 篇，按优先级展示前 200）
使用符号泰勒展开严格估计浮点舍入误差
提出符号泰勒展开方法并实现 FPTaylor，用严格全局优化更紧致地估计浮点最大舍入误差。
Cobblestone：一种自动化形式验证的分治方法
Cobblestone 用 LLM 分治合成 Coq 证明：拆分已验证子目标并迭代，保持可靠性，自动化形式验证。
基于大语言模型的证明自动化
提出 PALM：让 LLM 先生成证明，再用符号方法迭代修复低层错误，大幅提升 Coq 形式证明自动化成功率。
机器生成、机器检查的验证编译器证明（经验报告）
用 Claude Code 智能体从零机械化 CertiRocq 中 ANF 变换的语义保持证明，产出约 6000 行 Rocq 证明，耗时 94.5 小时。
Rango：面向自动化软件验证的自适应检索增强证明
提出 Rango，用检索增强的微调 LLM 在 Coq 中自动识别相关前提与相似证明，实现全自动证明合成。
Planning to Hammer：面向 Rocq 证明自动化的难度感知分解
Quarry 将证明规划与执行分离，用 LLM 提出分解并由难度模型排序，递归调用 CoqHammer 提升 Rocq 证明自动化。
Baldur：使用大型语言模型进行整体证明生成与修复
用微调大语言模型一次性生成完整证明，并借助失败尝试与错误信息修复，提升自动形式化验证能力。
基于 LLM 引导策略选择的自适应证明精化
提出 Adapt 框架，用 LLM 引导的决策器动态选择证明精化策略，显著提升定理证明的自动化成功率。
Proofs Promptly：用 AI Agent 进行面向证明的编程（经验报告）
经验报告：配备证明助手与 CLI 的 AI Agent 可自动产出数千行机器检验证明代码，把人类专家的工作压缩到给定问题描述与审查规约。
用正则表达式跟踪借用
提出以正则表达式跟踪访问路径的借用检查类型系统，经 Lean 机械化并部署于 Sui 的 Move 字节码验证器。
面向 Isabelle/HOL 神经定理证明的极简证明语言
提出极简证明语言 Minilang，并翻译 Isar 语料微调 LLM，以提升 Isabelle/HOL 神经定理证明性能。
多样性驱动的自动形式化验证
提出 Diva，通过训练多样化的证明脚本模型并结合搜索，显著提升 Coq 定理的自动证明率。
论证明的自然性
用语言模型分析 Coq 与 HOL Light 证明语料，发现证明具有高度可预测的语言规律性，补全可节省超 60% 输入。
ProofCoop：协作式自动形式化验证
提出 ProofCoop，让多个证明合成模型在搜索中协作，显著提升 Coq 定理自动证明成功率。
自动证明生成：Reasoner 与 Math LLM 中的微调与 RAG 对比
在 Isabelle/HOL 上比较数学 LLM、推理 LLM 及混合模型在基座、微调与 RAG 三种配置下的证明推断能力。
为交互式定理证明合成蕴含引理
基于数据驱动的不变式推断，在 Rocq 中自动合成蕴含形式的辅助引理以减轻交互式证明负担。
合则更强：统一 Datalog 与等式饱和
egglog 将 Datalog 与等式饱和（EqSat）统一为定点推理系统，兼具增量执行、同余闭包与项抽取能力。
Passport：利用标识符改进自动形式化验证
为证明合成模型的标识符引入类别词汇索引、子词序列建模与路径细化三种编码，自动证明的定理数最多提升 29%–45%。
PaMpeR：面向 Isabelle/HOL 的证明方法推荐系统
提出 PaMpeR，基于手写证明语料为 Isabelle/HOL 的证明状态推荐证明方法并给出定性解释。
工程化一个经过形式验证的自动缺陷查找器
提出用操作语义与符号语义关联来工程化可证明可靠且完备的符号执行缺陷查找器，并在 Coq 中验证 WiSE。
面向交互式证明的数据驱动引理合成
提出数据驱动的引理合成方法，将交互式证明中的辅助引理生成归约为程序合成，并实现为 Coq 策略 lfind。
抽象解释器：一种模块化验证的单子方法
提出以自由单子与处理器分层构建抽象解释器，并在 Coq 中模块化验证其可靠性。
概率编程语言的验证密度编译
提出 ProbCompCert：用 Coq 验证 Stan 子集概率编程语言编译器的关键遍，并发现 Stan 手册错误。
从带循环与条件化的概率程序到形式验证的采样器
提出经 Coq 形式验证的 Zar 编译器，将带循环与条件化的离散概率程序编译为正确采样器。
QEDCartographer：使用无奖励强化学习自动化形式验证
提出结合监督与无奖励强化学习的证明合成工具 QEDCartographer，利用证明分支结构提升 Coq 定理自动证明率。
构造性 Galois 连接
提出构造性 Galois 连接，使抽象解释中的 Galois 连接可在依赖类型证明助手中机械化并支持可提取算法。
Gpass：面向 Coq 的目标自适应神经定理证明器，用于自动化形式验证
提出基于 Coq 的目标自适应神经定理证明器 Gpass，显著提升自动形式验证中的定理证明性能。
正确性与性能兼顾：从 Agda 到 Futhark
用 Agda 形式化并抽取到 Futhark，使自动微分与 CNN 代码兼具正确性保证和接近 TensorFlow 的性能。
形式化 Linux eBPF 核心 ISA：机器化操作语义及其真实世界应用
在 Rocq 中形式化 eBPF 核心 ISA 的全部 153 条指令，并据此验证 eBPF 验证器抽象域的可靠性、发现内核缺陷。
版本化 E-Graph
提出版本化 E-Graph，同时编码多个等价集合与共享信息，并证明其正确性，显著提升条件等价场景性能。
交互式定理证明中战术库的自动发现
提出战术依赖图（TDG）驱动的战术发现方法，自动学习可复用战术并将证明重构得更模块化。
面向形式验证的元编程框架
在 Lean 中实现面向形式验证的元编程框架，通过反射对象级表达式支持高效编写 tactic 与自动化。
Mtac2：用于 Coq 中反向推理的类型化策略
提出 Mtac2，为 Coq 提供支持反向推理的类型化策略编程语言，可在策略定义期静态排除多类错误。
带合并的符号求值的形式化基础
首次为支持状态合并的可复用符号求值器建立形式语义，并在 Lean 中机械化证明其可靠性与完备性。
WasmRef-Isabelle：一个经验证的 WebAssembly 单子解释器与工业级模糊测试预言机
在 Isabelle/HOL 中实现并机器化验证 WebAssembly 单子解释器，作为 Wasmtime 的模糊测试预言机，兼顾规范对应性与性能。
使用 Kripke 规约单子的经过验证的符号执行（且无需元编程）
提出基于 Kripke 规约单子构造符号执行验证器并证明其可靠性的系统方法，在 Katamaran 中全验证实现。
模式化数据竞争自由
扩展 OCaml 类型系统，以 mode 保证多线程数据竞争自由并兼容顺序代码。
面向已验证库的半自动化证明修复
提出首个高阶命令式函数的证明修复方法，在 Coq 中结合动态对齐和不变量综合，自动生成大部分证明并留下少量残余义务。
CSim²：Isabelle/HOL 中基于 rely-guarantee 的并发系统组合式自顶向下验证框架
在 Isabelle/HOL 中提出组合式 rely-guarantee 仿真框架 CSim²，将并发系统高层规约的性质自顶向下保持到实现层。
SpaceSearch：用于构建和验证求解器辅助工具的库
提出 Coq 库 SpaceSearch，让用户在证明助手中构建并验证求解器辅助工具，再提取到 Rosette 高效执行。
HoCHC：一个反驳完备且语义不变的高阶逻辑模理论系统
为高阶约束 Horn 子句提出简单归结证明系统，并证明其在标准与 Henkin 语义下可靠且反驳完备。
有根基的多模态程序验证器
提出基于 Lean 的框架，用 monad transformer 代数自动导出可靠的验证条件生成器，以构建有根基的多模态程序验证器。
Tree Borrows（树状借用）
用树结构替代栈定义 Rust 别名模型 Tree Borrows，更精确刻画 unsafe 代码行为，大幅减少误报并保留与新增编译器优化。
面向 Coq 的变异分析
提出变异证明技术并实现 mCoq，通过变异 Coq 定义检验证明是否失败，以评估和改进证明工程。
差分隐私的已验证基础
在 Lean 中机械化差分隐私基础，并提供经形式验证的 Laplace 与高斯采样实现。
VMSL：面向通过 FF-A 通信的虚拟机机械化鲁棒安全性的分离逻辑
提出分离逻辑 VMSL，可模块化推理 FF-A hypercall ABI 上通信的虚拟机并机械化证明其鲁棒安全性。
PureCake：一个经验证的惰性函数式语言编译器
首个端到端机器验证的惰性函数式语言编译器，将 PureLang 编译到机器码并在 HOL4 中完成正确性证明。
超越正确性：通过多步自动定理证明揭示 LLM 生成推理中的逻辑缺陷
提出 MATP 框架，将 LLM 自然语言推理转为 FOL 并用自动定理证明逐步检测逻辑错误。
用于 SAT 求解器-精化器通信的灵活证明格式
提出 FRAT 证明格式与工具链，显著降低 UNSAT SAT 证明精化为 LRAT 的时间与内存开销。
带公理的正交逻辑
为带公理的正交逻辑建立证明论，给出广义切消、三次时间判定算法及其与有界宽度消解和 Datalog 扩展的关系。
自动分离逻辑验证器中的保持验证的内联
提出首个用于自动分离逻辑验证器的保持验证内联技术，并给出经 Isabelle/HOL 验证的语义条件。
BFF：位域操作程序的基础化与自动化验证
提出 BFF，在 Coq 中机械化地对位域操作的 C 系统代码实现既自动化又有形式语义基础的正确性验证。
兴趣分歧的模拟关系家族
提出 μdiv-模拟关系，统一强、弱、发散敏感等 12 种模拟，并在 Rocq 中形式化验证。
面向程序验证的模块化、代码特化与零开销抽象
在 F* 的 Low* 工具链中提出语言技术，使高层模块化验证代码可特化并编译为零开销 C 代码。
走向交互式定理证明器中纸笔风格的等式推理：基于等式饱和的方法
将定理解释为条件重写规则，用 e-graph 等式饱和在 Lean 中实现纸笔风格的等式推理 tactic。
不相等/相等图（Dis/Equality Graphs）
首次形式化直接支持不等式的 e-graph，证明其比等式嵌入编码更高效，并在 egg 中实现验证。
P4-SpecTec：将语言机械化框架集成到真实世界 P4 规范中
提出 P4-SpecTec，用可执行算法推理规则机械化 P4 静态/动态语义，生成类型检查器与解释器，发现 24 个 bug。
形式化验证的二进制级指针分析
提出形式化证明正确的二进制级指针分析，并用通用抽象域证明义务支持不同精度实例化。
面向未来 700 种内存模型的组合符号执行
为可参数化内存模型的组合符号执行平台提供新形式基础，并在 Rocq 中机器化。
面向机器化程序验证的结构化时序逻辑
提出结构化时序逻辑 ticl，将复杂（余）归纳证明编码为结构引理，在证明助手中以高抽象层次对无限程序的安全性/活性进行组合式验证。
等价超图：幺半群 E-Graph 的 DPO 重写
为幺半群 e-graph 建立范畴语义与 e-超图表示，并实现 DPO 重写。
导航 AND–OR 图修改以调试失败的证明搜索
将 AND–OR 图视为证明系统的部分表示，把失败证明搜索的调试转化为修改证明系统，并统一 why-not 策略。
嵌套归纳类型：Lean 与 Rocq 中有依据且可用的嵌套归纳类型
提出嵌套归纳类型的有效性判据，保证可展开为互归纳类型，并自动生成正确的消去原理。
在你选择的交互式定理证明器中进行组合式神经-信息物理系统验证
提出 Vehicle 的组合式方法，将神经网络验证与符号证明集成到任意交互式定理证明器中。
不动点方程系统上的操作
研究完备格上不动点方程系统在变量代入、方程重排等操作下解保持不变的条件，并提供机器检查证明。
从零构建 Iris：高阶并发分离逻辑的模块化基础
以第一性原理统一、完整地阐述 Iris 3.1 的设计与语义基础，为高阶并发分离逻辑奠定模块化框架。
ARMv8-A、RISC-V 和 CHERI-MIPS 的 ISA 语义
使用 Sail 语言为 ARMv8-A、RISC-V、MIPS 和 CHERI-MIPS 架构建立严谨的可执行语义模型，支持模拟器与证明助手代码生成。
交互树：在 Coq 中表示递归与不纯程序
提出交互树，在 Coq 中表示递归、有副作用且可能非终止的程序，支持组合解释与弱互模拟等式推理。
面向以太坊虚拟机字节码的形式化验证工具
基于KEVM形式语义与K框架可达性逻辑，构建并优化了EVM字节码演绎验证器，成功验证多个知名智能合约。
MoSeL：面向分离逻辑交互式证明的通用可扩展模态框架
提出 MoSeL，一个通用可扩展的 Coq 框架，将 Iris 证明模式推广到更广泛的分离逻辑。
单态与多态类型的编码
系统研究并实现将单态与多态类型编码到无类型一阶逻辑的方案，提升自动定理证明效率且保持可靠完备。
Cubical Agda：一种支持 univalence 与高阶归纳类型的依赖类型编程语言
通过 cubical 原语扩展 Agda，使其原生支持 univalence 与高阶归纳类型并保持构造性。
Stacked Borrows：一种面向 Rust 的别名模型
提出 Stacked Borrows 操作语义，为 Rust 定义别名纪律，并用 Coq 证明其足以支撑内存访问重排优化。
RefinedRust：面向 Rust 程序高保障验证的类型系统
提出在 Coq 中证明可靠的精化类型系统，支持 safe 与 unsafe Rust 代码的基础性半自动功能正确性验证。
使用 Idris 进行类型驱动开发
介绍 Idris 中依赖类型驱动的开发方法，面向工程师，涵盖函数式编程、依赖类型与程序验证。
LLVM IR 的模块化、组合式且可执行的形式语义
用 Coq 中 interaction trees 的单子解释为 LLVM IR 大型顺序子集建立模块化、可组合且可执行的形式语义。
带时间信用的分离逻辑中的 thunk 与 debit
在 Iris 时间信用分离逻辑中机器化重建 Okasaki 的 thunk/debit 摊还推理规则，并验证流与多种队列。
JIT 编译器中形式化验证的推测与去优化
提出显式化去优化同步点与推测假设的 JIT 中间表示，并在证明助手中验证若干推测优化。
一种经验证、高效的可验证汇编语言嵌入
在 F* 中嵌入 x64 汇编子集，借助依赖类型检查器运行经验证的 VC 生成器，实现汇编与 C 互操作的高效验证。
并发随机化程序的分离逻辑
提出支持概率推理的并发分离逻辑 Polaris，并机器化验证随机化并发计数器与跳表。
在类型论中实现类型论的正规化求值
在类型论内部用商归纳类型构造依赖类型的正规化求值，并证明定义相等可判定。
顺序程序的分离逻辑（functional pearl）
提出面向顺序程序分离逻辑的简易机器化形式化，用于教学并覆盖可靠性证明与近期扩展。
POPLMark 重装上阵：通过逻辑关系机械化证明
提出用Kripke式逻辑关系证明强规范化的基准，比较Beluga、Coq、Agda等证明助手对机械化元理论的支持。
超 Hoare 逻辑：（反）证明程序超性质
提出超 Hoare 逻辑，将断言提升到状态集合，可在同一逻辑中证明和反证程序超性质。
Narcissus：从二进制格式构造即正确地推导解码器与编码器
用 Coq 策略从无冗余二进制格式规范自动推导互为逆的解码器与编码器，并重实现网络协议栈。
底层沙箱化的高层收益
证明沙箱化可使受信任代码在任意不可信代码存在时仍保持类型安全（鲁棒安全），并在Coq中机械化验证。
Cedar：一种表达力强、快速、安全且可分析的授权语言
提出授权策略语言 Cedar，兼顾可读性、快速求值、安全与可分析性，并开源实现。
带续延的并发程序的机械化关系验证
首个全形式化工具，机械化关系验证带 call/cc 与 throw 的并发高阶命令式程序。
一个成本感知的逻辑框架
提出 calf 成本感知逻辑框架，以依赖类型论统一程序行为与成本推理，并在 Agda 中机器化验证算法复杂度。
驯服重写：一种带计算假设的类型论
提出重写类型论 RTT，允许把计算假设写成重写规则并自动用于类型检查，同时保持类型可靠性。
预备，开始，验证！将 hs-to-coq 应用于真实 Haskell 代码（经验报告）
将 Haskell containers 库翻译到 Coq 并验证，证明可验证成熟、未修改的函数式代码。
带重置的数据流同步语言的机器化语义与经过验证的编译
在 Coq 中为带 reset 原语的数据流同步语言扩展机器化语义，并证明其编译器各趟的正确性。
Choice Trees：在 Coq 中表示非确定性、递归与不纯程序
提出 ctrees，一个在 Coq 中统一建模非确定性、递归与不纯程序并支持双模拟/精化推理的余归纳树单子。
Arm® 机密计算架构的验证方法：从安全规约到安全实现
提出结合交互式定理证明、模型检测与并发测试的方法，验证 Arm CCA 中 RMM 的规约与原型实现。
Iris-Wasm：WebAssembly 程序的鲁棒模块化验证
提出 Iris-Wasm，在 Coq/Iris 中为 Wasm 1.0 建立高阶分离逻辑，支持模块化验证与鲁棒安全。
Steel：依赖类型并发分离逻辑中的面向证明的编程
在依赖类型语言 F* 中提出 Steel，用五元组 Hoare 逻辑把并发程序与其分离逻辑证明协同开发。
Iron：管理高阶并发分离逻辑中的义务
提出 Iron，一种高阶并发分离逻辑，可精确推理动态线程间可转移资源及其义务，并在 Iris 模型与 Coq 中证明其可靠性。
从 Coq 到 OCaml 的已验证提取
在 Coq 中实现并验证从 Coq 到 OCaml 的提取流水线，给出正确性定理与安全互操作保证。
经验证的量子 oracle 编译
提出 Coq 中实现的高保障框架 VQO，形式验证从 OQIMP 到 OQASM 再到 SQIR 的量子 oracle 编译器，并用 QFT 降低量子比特开销。
一个合理异常的类型论
提出三层 RETT，在完全依赖类型论中首次一致地推理异常项，并提供 Coq 插件 CoqRETT。
虚拟时间线：一种验证具有时间隔离的抢占式调度器的形式化抽象
提出虚拟时间线抽象，并在 Coq 中验证抢占式调度器实现，使实时内核获得时间与空间隔离。
烤蛋糕的蛋糕：CakeML 中的动态计算
为已验证的 CakeML 编译器加入 Eval 原语，实现运行时代码求值与动态执行，并支持首个可验证的 LCF 风格定理证明器运行时环境。
Tachis：面向期望代价的带信用额度的高阶分离逻辑
提出 Tachis，一种带概率代价信用（cost credits）的高阶分离逻辑，用于证明概率程序的期望代价上界。
一个用于验证 CompCert C 程序的 Iris 实例
在 Iris 中构建基于 CompCert 语义的分离逻辑实例，以验证 C 程序正确性。
带宇宙与擦除的分级模态依赖类型理论及其形式化
提出带宇宙与擦除的分级模态依赖类型理论，并在 Agda 中形式化，证明元理论性质与擦除提取的可靠性。
高效完全高阶合一
提出高效完全高阶合一过程，通过限制搜索空间与集成片段判定，在 Zipperposition 中实现并优于已有方法。
Futhark 中高阶模块的静态解释：面向大规模的函数式 GPU 编程
为纯函数式数据并行语言 Futhark 设计高阶模块系统，并在 Coq 中形式化其静态语义与编译期消除。
结构化数据的机械化 Hypersafety 证明
提出 LGTM：参数化 Hypersafety 关系分离逻辑，并在 Coq 中机械化验证结构化数据操作。
为语言无关的演绎程序验证器生成证明证书
为语言无关演绎验证器生成可独立检验的证明证书，以认证每次成功验证的正确性。
关系式 e-matching
提出基于关系连接与查询计划的 e-matching，保证最坏情况最优运行时间，并在 egg 中大幅加速。
LLF_𝒫：一个使用 monad 建模外部证据、边条件与证明无关性的逻辑框架
扩展 LF 提出 Lax Logical Framework LLF_𝒫，用 Lock monad 表达边条件、外部证据与证明无关性，并证明其保守性。
面向 CIC 的新合一器可理解指南：包含宇宙多态与重载
完整描述并实现支持宇宙多态与重载（规范结构）的 CIC 合一算法，并在大型库上验证启发式足够。
CHERI C 的形式化机器化语义：能力、未定义行为与来源
首次严格全面地定义 CHERI C 语义，涵盖能力、来源与未定义行为，并给出可执行及 Coq 机器化形式。
VST-A：一个基础可靠的注解验证器
提出 VST-A，一个基于 VST 丰富断言语言和 Coq 可靠证明的注解验证器，可将 C 函数验证归约为直线 Hoare 三元组。
CCLemma：E-Graph 引导的归纳等式证明中的引理发现
提出 e-graph 引导的引理发现，使理论探索目标导向，提升归纳等式证明的效率和能力。
软件模型检测作为循环证明搜索
将多种软件模型检测算法统一为循环证明系统中的证明搜索策略，并揭示极大保守性启发式的意义。
证明相关的合一：仅使用你的类型论公理的依赖模式匹配
提出证明相关的合一框架，使合一规则只依赖所在类型论自身的公理，并据此重写 Agda 的合一算法修复大量缺陷。
自动化 Dirac 记号中的等式证明
证明 Dirac 记号的一阶理论可判定，并用项重写高效判定等式，实现等价性检查器。
在 Coq 中形式化 Core Why3
在 Coq 中为 Why3 逻辑片段建立形式语义，并机器化验证其证明系统与变换的可靠性。
引导式等式饱和
提出引导式等式饱和，将复杂重写拆成经人工中间引导连接的自动等式饱和步骤，提升可扩展性。
通过族多态实现可扩展的元理论机械化
提出基于族多态的语言设计，使证明助手能复用和扩展元理论机械化代码与证明。
如何用二阶计算分析器 SOL 证明等式理论的可判定性
提出二阶代数理论下证明等式理论可判定性的通用方法，并实现 Haskell 分析器 SOL。
D<: 的不可判定性及其可判定片段
证明 D<: 的类型检查与子类型不可判定，并给出两个可判定片段与判定算法。
密码学服务器的基础性集成验证
在 Coq 中整合多种验证技术，端到端证明裸机密码学服务器的全系统功能正确性与内存上界。
JavaScript 正则表达式语义的 Coq 机器化
首次在 Coq 中忠实机器化 ECMA-262 的 JavaScript 正则语义，证明匹配必然终止且安全，并可提取为通过 Test262 的引擎。
Call-by-Push-Value 中的效应与余效应
将效应与余效应追踪引入 CBPV 类型系统，证明其可靠性并在 Coq 中机器化验证。
分离逻辑中线性化的证明自动化
在 Iris 中为线性化的上下文精化与逻辑原子性证明开发可扩展的 Coq 自动化，显著减少证明工作量。
依赖类型理论的可扩展相等性检查算法
提出一种用户可扩展的相等性检查算法，适用于一大类依赖类型理论，并在 Andromeda 2 中实现。
概率重写与渐近行为：终止性与唯一范式
为概率重写系统建立分析终止性、唯一极限分布与唯一范式的证明技术，并用于比较归约策略。
论单子式逆向归纳的正确性
定义单子式 SDP 的正确性，给出三个条件证明单子逆向归纳正确，并在 Idris 中形式化。
量子比特回收再审视
提出量子比特依赖图，将量子比特回收归约为矩阵三角化，给出 NP 难性、启发式求解器与 Coq 验证实现。
“do”解缚：在纯函数式语言中拥抱局部命令式（函数式珍珠）
为纯函数式语言的 do 记法加入局部可变、提前返回与迭代，并给出到纯函数代码的翻译及 Lean 正确性证明。
从重写规则推导高效程序变换
提出在 Coq 中从重写规则与辅助数据结构规约半自动推导高效程序变换及其正确性证明的系统。
使用 Coq 原型化查询编译器（经验报告）
报告用 Coq 证明助手原型化查询编译器并移植到 Java 的工业经验与利弊。
piCoq：面向大规模验证项目的并行回归证明
提出融合并行证明检查与回归选择的技术及工具 piCoq，显著加速 Coq 大规模验证项目的证明检查。
良括号控制流的逻辑本质
提出首个基于分离逻辑的 Hoare 式程序逻辑，用于推理良括号控制流，并在 Coq/Iris 中机械化。
在 Coq 中从 Coq 提取函数式程序
在 Coq 内构建认证提取管线，将依赖类型程序翻译为多种函数式语言并验证关键变换。
面向健壮性的必要性规约
提出 Necessity 语言，用必要性算子刻画时序蕴含，从功能规约推导健壮性规约并在 Coq 中机械化验证可靠性。
外延相等保持与已验证泛型编程
提出外延相等保持原则，在内涵类型论中无需扩展理论或完整 setoid 即可进行已验证泛型编程。
基于不可满足性证明的带关系对象一阶逻辑诊断
为 FOL* 不可满足性结果定义证明格式与规则，并给出证明校验与基于证明的诊断方法，用以解释不可满足的成因。
论插值算法的完备性
首次系统研究插值算法的完备性，证明若干归结与相继式演算标准插值算法的不完备性及多种完备性。
ArchSem：可复用的宽松架构严格语义
提出架构通用框架 ArchSem，模块化组合 ISA 与并发模型，并在 Rocq/Isabelle 中实例化 Arm/RISC-V 以支持严格验证。
QuickSub：高效的同构递归子类型判定
提出高效易实现的同构递归子类型算法 QuickSub，最坏复杂度 O(nm)，常见情况近线性，并用 Coq 形式化验证。
程序逻辑 à la carte
通过组合可复用的程序逻辑片段，实现跨语言及语言内模块化定义并证明程序逻辑。
检查无限下降的复杂性景观
在逻辑无关的抽象框架下，系统刻画循环证明无限下降检查准则的参数化复杂度，并提出改进算法。
融入语义性质的结合交换同余闭包算法的模块化与组合
提出模块化 AC 同余闭包算法，可组合幂等、可消去、群等语义性质，便于集成到 SMT 求解器。
无界分离逻辑中的分数资源
提出允许断言求值期间持有超过完整权限的无界分离逻辑语义，统一语义与语法乘法并恢复分配、提取与合并性质。
参数化转换演算与可复用的渐进类型lambda演算元理论
提出两个参数化转换演算与可复用元理论，统一渐进类型lambda演算变体并在Agda中机械化。
线性终止是不可判定的
通过从希尔伯特第十问题归约，证明单规则重写系统线性解释终止性不可判定，并扩展至多种序与多项式解释。
模群（Groups）的同余闭包
提出模群公理的同余闭包框架，通过等式完成过程构造基收敛重写系统，并在终止时判定相关字问题。
符号自动机：模理论下的 ω-正则性
将符号自动机从有限字推广到 ω-正则语言，统一交替/非确定 Büchi 自动机与 LTL、PSL 的模理论框架。
用三维精化代数统一组合式验证与认证编译
提出三维精化代数及其组合语义框架，并在 Coq 中统一组合式验证与认证编译。
用于高效 WebAssembly 机器化的 Progressful 解释器
提出 progressful 解释器，用 Coq 依赖类型认证健全性与 progress，高效扩展 Wasm 2.0 机器化。
Quiver：在 Coq 中引导式溯因推断分离逻辑规约
提出 Quiver，在 Coq 中以用户规约草图为引导，溯因推断分离逻辑功能正确性规约并同时进行基础性验证。
交互式证明助手中的实时验证
在Coq中实现实时验证原型：逐行显示符号状态，并用diff形式表达循环不变式，边写代码边生成机器检查证明。
类型推断逻辑
提出一套逻辑框架，使约束式类型推断与elaboration能在Coq中模块化地机器验证其可靠性与完备性。
最小计算集合论中的适用数学
扩展静态逻辑框架，证明最小谓词主义无限集理论是计算性的，且足以形式化大部分科学适用数学。
Graphiti：数据流电路中形式化验证的乱序执行
在 Lean 4 中建立数据流电路的图精化元理论，并形式化验证引入乱序执行的循环重写，性能与未验证方法持平。
Trocq：超越等价与 univalence 的免费证明转移
提出 Trocq 证明转移框架，基于新的类型等价表述推广 univalent parametricity，并实现为 Coq 插件。
情境中的 QED：一项针对证明助手用户的观察研究
通过情境访谈观察 30 名 Rocq 和 Lean 用户，揭示证明助手实际使用中的迭代、对话、外部资源与超越 QED 的设计诉求。
Morello-Cerise：Arm Morello 能力硬件架构的强封装性证明
在 Morello ISA 全规模模型上机器化证明任意不可信代码存在时软件组件的强安全封装性质。
Nola：用于在 Iris 中验证终止性的无 later 模态幽灵状态
提出 Nola 框架实现无 later 模态的高阶幽灵状态，支撑 Iris 中对 Rust 程序终止性等完全正确性的验证。
盒子里有什么：面向泛型数据结构的人机工程学与表达力兼备的捕获跟踪
提出 System Capless 与 reach capabilities，使捕获类型能跟踪泛型数据结构内的能力，并在 Scala 3 中实现与验证。
基于已验证位爆破的交互式位向量推理
提出首个端到端已验证的位爆破器 bv_decide，将高效位向量推理作为 Lean 交互式证明 tactic，并支持反例生成。
形式化图变换的双推出（DPO）方法
在 Isabelle/HOL 中形式化双推出图变换基础理论，并机器验证推导唯一性与 Church-Rosser 定理。
代数效应在 Cubical Agda 中遇上 Hoare 逻辑
在 Cubical Agda 中用商类型形式化带方程的代数效应，并提供效应通用的 Hoare 逻辑与等式推理。
Cubical Agda 的内部参数性与观察式参数性
提出首个实用的内部参数性证明助手 Agda--bridges，并基于 SRP 给出内部自由定理的单行证明。
Shoggoth：策略重写的形式化基础
提出 Shoggoth，为策略重写建立指称语义与基于位置的弱前置条件演算，并在 Isabelle/HOL 中机化验证。
一种用于计算机代数的安全低级语言及其形式验证编译器
提出一种介于 C 与 Rust 之间、面向计算机代数底层库的安全低级语言，并用 Coq 证明其安全性及基于 CompCert 的编译器语义保持。
完全验证的指令调度
提出首个完全验证指令调度的机械化证明库，将证明负担降到交换相邻独立指令的语义保持。
合并归纳关系
提出合并共享索引的归纳关系的算法，生成等价合取关系，显著提升自动生成性能并简化 Coq 机械化证明。
超越回溯：细粒度并发分离逻辑中的连接
提出基于连接演算的多后继分离逻辑演算，在 Coq/Iris 中实现，减少回溯并自动验证细粒度并发程序。
显式精化类型
提出 λert 类型理论，让程序员显式嵌入精化性质的证明，从而支持量词和归纳，并用 Lean 4 证明其可靠性。
Coq 中的可计算分析与连续性概念
在 Coq 中基于 Incone 库形式化可计算分析，给出连续结构上可执行算法的正确性证明。
Scala 的一等精化类型
为 Scala 3 设计一等精化类型，使精化与子类型、推断、模式匹配统一整合，并机化证明核心演算的类型可靠性。
基于构造性实数的全局优化
在构造类型论与可计算实数下建立全局优化与回归的联系，并给出收敛准则及 Agda 机器化证明。
最优重写公式与数据库查询：项重写、结构分解与复杂度的交汇
该论文为正向一阶公式在常见等价保持重写规则下的宽度最小化给出完备算法，连接项重写、查询求值与结构分解。
在立方类型论中自动化边界填充
提出面向立方类型论的边界填充自动化方法，统一求解 contortion 与 Kan 问题，并实现 Haskell 求解器。
Coco：组合式异构生产性的余递归
提出 CHP 框架与 Rocq 库 Coco，通过组合式异构生产性自动化支持广泛余递归定义。
增量计算中的有状态差分算子
提出有状态差分算子的形式规约，在 Rocq 中机械化验证，可指导新算子设计并刻画 join 与 Datalog 聚合等既有算子。
既要编码又要吃到蛋糕：在类型论中局部地控制计算
提出 LRTT 类型理论，以局部抽象封装用户自定义计算规则，并给出保守性证明与 Rocq 原型。
面向契约满足证明的演绎系统
提出相对轨迹相等问题与相对互模拟技术，给出可靠完备的演绎证明系统，并在Rocq中形式化用于CPU契约满足证明。
CRIS：混合验证中的想象力
提出 imaginary specifications，将可执行代码与所有权断言自由混合，并构建 CRIS 框架推广 CCR，支持对未验证代码副作用的模块化推理。
因果性与语义分离
在 Rocq 中机器化证明 d-separation 与受非干扰启发的语义定义等价，为实验设计验证提供语义基础。
Let It Flow：异步数据流的形式化验证编译框架
首个对异步数据流编译器进行形式化验证的工作，用能力类型系统与 Lean 机器化证明同时保证确定性与流水线优化。
依赖类型论中单子等式推理的实用形式化
在 Coq 中以接口方式形式化效应单子层级与代数律，使单子等式推理可机器化并实用化。
可扩展语言元理论推理的模块化方法
提出可扩展语言的模块化元理论方法，按语言片段分解证明并对扩展做通用推理，并实现于 Sterling/Extensibella。
认证编译器 à la carte
为 Rocq 引入晚绑定、mixin 组合与族多态的扩展机制（Rocqet 插件），使 CompCert 级别的认证编译器可模块化、可复用、按需组合。
Slotted E-Graph：为（绑定）变量提供一等支持
提出槽位 E-Graph，将绑定变量作为内建一等特性，使仅变量名不同的项共享表示，避免 E-Graph 膨胀。
McTT：一个经过验证的证明助手内核
提出并实现 McTT，一个在 Rocq 中验证、可提取为 OCaml 的 Martin-Löf 类型论内核。
虚拟化内存地址的模态抽象
提出模态断言 [r]P 与虚拟 points-to 断言，在 Rocq 中验证多地址空间 x86-64 虚拟内存管理代码。
宽度无关位向量谓词的已验证判定过程
在 Lean 中机械化模型检测与 MBA-Blast 算法，为宽度无关位向量谓词提供可扩展的已验证判定过程。
SAT 启发的高阶消去技术
将多种命题预处理消去技术推广到高阶逻辑，提出拟纯文字消去，并在 Zipperposition 中提升自动证明搜索。
Riesz 空间与模态 Riesz 空间的证明论
为 Riesz 空间与模态 Riesz 空间设计超序列演算，证明可靠、完备与切消，并据此给出模态 Riesz 空间可判定性的新证明。
Coq 中的希尔伯特第十问题（扩展版）
在 Coq 中完成 DPRM 定理的首次完整机器化证明，形式化了希尔伯特第十问题的不可判定性。
用于概率与非确定性公理化推理的可信 monad
在 Coq 中形式化几何凸单子，为概率与非确定性选择的等式推理提供可信模型和可复用理论。
三值几何归结中的包含算法
将三值几何归结的包含/匹配归约为广义约束满足，提出直接算法、SAT 编码与局部一致性过滤。
翻译式分离逻辑验证器中的可靠状态编码
提出首个支持非平凡状态编码的翻译式分离逻辑验证器可靠性形式化框架，并以 Isabelle/HOL 机器化验证。
全自动测试定理
提出一种全自动、鲁棒于等价表述的定理性质测试策略，把生成器搜索建模为约束调度问题。
将基础验证引入真实世界的 Rust 代码
扩展 RefinedRust 以支持 trait、闭包和迭代器等高级抽象并与 unsafe 代码结合，从而对真实 Rust 代码进行基础验证。