A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs
我们认为，功能性程序设计语言的编译器的实现和验证大大简化了采用高阶表示的语法称为高阶抽象语法或HOAS。HOAS的基本思想是使用一种元语言，它为绑定相关概念提供内置的逻辑处理。通过将元语言嵌入到更大的编程或推理框架中，可以将对象语言中的绑定结构的处理吸收到系统的元理论中，从而大大简化整体实现和推理过程。我们在这篇论文中提出并证明了上述论点的有效性的方法来验证执行的编译器转换的函数程序，利用HOAS。在这种方法中，函数程序的转换首先以基于规则的关系规范的形式表达。这些规范被渲染成语言lambda Prolog的程序。一方面，这些程序直接作为实现。另一方面，它们可以用作Abella系统的输入，该系统允许我们证明关于它们的属性，从而证明关于实现的属性。lambda Prolog和Abella都支持使用HOAS方法。因此，它们构成了一个框架，可用于在验证编译中测试HOAS方法的好处。我们用它们来实现和验证一个编译器的代表性的功能程序设计语言，体现了许多编译器的核心，这些语言的转换。在这两个编程和推理阶段，我们展示了如何使用的HOAS方法显着简化了绑定结构的表示，操作，分析和推理。
2017-02-11 cs.LO cs.PL
Let it Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow
Carnegie Mellon University（卡内基梅隆大学）；University of Maryland, College Park（马里兰大学帕克分校）
该研究提出首个异步数据流编译器的形式化验证框架Wavelet，通过带围栏的能力类型系统等技术，验证编译器核心 passes 并证明相关属性，编译的数据流图规模与未经验证编译器相当。
2026-08-07 cs.LO cs.PL
TRX: A Formally Verified Parser Interpreter
语法分析是计算机科学中的一个重要问题，然而令人惊讶的是，很少有人关注它的形式化验证。在本文中，我们提出了TRX：解析器解释器正式开发的证明助手Coq，能够产生正式正确的解析器。我们正在使用解析表达式语法（PEG），一种形式主义，基本上代表递归下降解析，我们认为这是一个有吸引力的替代上下文无关文法（CFG）。从这种形式化中，我们可以提取出一个任意PEG语法的解析器，保证完全正确，即，所得到的解析器在其语法和PEG的语义方面是终止的和正确的;这两个属性在Coq中被正式证明。
2011-06-22 cs.FL cs.LO cs.PL
Formally Verified SAT-Based AI Planning
我们提出了一个可执行的正式验证SAT编码的经典AI规划。我们使用定理证明器Isabelle/HOL进行验证。我们实验测试验证编码，并表明它可以用于合理大小的标准规划基准。我们还使用它作为参考来测试最先进的基于SAT的规划器，表明它有时会错误地声称问题没有一定长度的解决方案。
2023-03-07 cs.AI cs.LO
QED at Large: A Survey of Engineering of Formally Verified Software
开发程序正确性的形式化证明可以增加实际和感知的可靠性，并有助于更好地理解程序规范及其基本假设。支持这种发展的工具已有40多年的历史，但直到最近才得到广泛的实际使用。基于机器检查的形式化证明的构建的项目现在达到了前所未有的规模，可以与大型软件项目相媲美，这导致了证明开发和维护的新挑战。尽管其日益重要，证明工程领域很少考虑自己的权利;相关的理论，技术和工具跨越许多领域和场所。这篇文献综述对程序正确性的证明工程有了全面的了解，包括在实践中的影响、基础、证明自动化、证明组织和实际证明开发。
2020-03-13 cs.LO cs.PL
Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes
我们正式验证可执行算法解决马尔可夫决策过程（MDPs）的互动定理证明器伊莎贝尔/HOL。我们建立在现有的形式化的概率论分析的期望总回报准则的无限地平线的问题。我们的发展形式化的贝尔曼方程，并给出最优政策存在的条件。在此基础上，我们验证了动态规划算法来解决表MDP。我们评估正式验证的标准问题的实验实现，并表明他们是实用的。此外，我们表明，结合有效的未经验证的实现，我们的系统可以竞争，甚至优于最先进的系统。
2023-03-08 cs.AI cs.LO
Logical Relations for Formally Verified Authenticated Data Structures
本文提出基于新型关系分离逻辑的形式化证明方法，为可自动生成认证数据结构的库验证安全性与正确性，证明了库优化的正确性及手写实现与自动生成代码的可靠链接，结果已在Coq中通过Iris框架机械化验证。
2025-01-18 cs.LO cs.PL
Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL
仿真和形式化验证是基于模型的高可靠性系统开发的重要补充技术。为了支持一致的结果，有必要为这两个活动提供统一的语义和自动化。在本文中，我们应用Isabelle/HOL中的交互树产生一个验证和仿真框架的状态丰富的过程语言。我们开发的核心理论和验证技术的交互树，使用它们给CSP和马戏团的语言的语义，并正式连接我们的新语义与故障分歧的语义模型。我们还展示了如何伊莎贝尔代码生成器可以用来生成验证可执行的模拟反应和并发程序。
2021-05-11 cs.LO
A Formally Verified Procedure for Width Inference in FIRRTL
Key Laboratory of System Software (Chinese Academy of Sciences)（系统软件重点实验室）；Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；University of Chinese Academy of Sciences（中国科学院大学）；Nanjing Institute of Software Technology（南京软件工程研究所）；Birkbeck, University of London（伦敦大学伯贝克学院）
本文提出了一种正式验证的FIRRTL宽度推断过程，通过定理证明器Rocq实现，并在OCaml中提取出首个正式验证的InferWidths阶段实现。
2026-01-19 cs.LO cs.PL
A formally verified proof of the prime number theorem
1896年由阿达玛和德·拉·瓦莱·普桑独立建立的素数定理断言，正整数中素数的密度渐近于1 / ln x。虽然他们的证明认真使用的方法复杂的分析，小学的证明提供了塞尔伯格和埃尔德奥斯在1948年。我们描述了一个正式验证版本的Selberg的证明，获得使用伊莎贝尔证明助手。
2006-04-06 cs.AI cs.LO cs.SC
Formal Semantics and Formally Verified Validation for Temporal Planning
Techniche Universität München（慕尼黑工业大学）；King’s College London（伦敦国王学院）
我们提出了一个简单而简洁的语义时间规划。我们的语义开发和形式化的逻辑的互动定理证明伊莎贝尔/HOL。我们从这些语义的验证算法的时间规划和显示，使用Isabelle/HOL的正式证明，该验证算法实现我们的语义。我们通过实验评估我们验证的验证算法，并表明它是实用的。
2022-03-25 cs.AI cs.LO
Formally Verified Certification of Unsolvability of Temporal Planning Problems
本文提出将时序规划问题编码为时间自动机网络，结合模型检查器与经 Isabelle/HOL 形式化验证的证书检查器，为不可解性结论提供高可信认证。
2025-10-19 cs.AI cs.LO
A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
本研究提出一种经形式化验证的MDP区间迭代浮点实现，通过Isabelle/HOL完成从抽象语义到LLVM代码的全链路正确性证明，扩展精化框架支持浮点推理，实验表明其性能与前沿工具相当且具备形式化正确性保证。
2025-10-06 cs.LO
A formally verified proof of the Central Limit Theorem
我们描述了一个证明的中心极限定理，已正式核实的伊莎贝尔证明助手。我们的形式化的基础上，并扩展伊莎贝尔的图书馆分析和测量理论的概率。该定理的证明使用特征函数，这是一种傅立叶变换，以证明，在适当的假设下，随机变量的总和弱收敛到标准正态分布。我们还讨论了支持正式化的库和基础设施，并反思了我们从这一努力中吸取的一些教训。
2017-02-01 cs.LO cs.MS math.PR
Duality theory in linear optimization and its extensions -- formally verified
Institute of Science and Technology Austria（奥地利科学技术研究所）
本文通过形式化证明，扩展了Farkas定理至线性有序域，并探讨了允许系数取无限值的对偶理论扩展。
2026-03-06 cs.LO math.OC
A Formally Verified HOL Algebra for Dynamic Reliability Block Diagrams
为了克服传统可靠性框图无法捕捉冗余元件等建模缺陷，引入了动态可靠性框图（DRBDs）。然而，到目前为止，还没有一个代数框架，允许进行分析的一个给定的DRBD的基础上，其结构功能，并能够验证其可靠性使用高阶逻辑（HOL）定理证明。在这项工作中，我们提出了一个新的代数正式表示的结构功能和可靠性的DRBD与备用构造的基础上的基本系统块和新引入的DRBD运营商。我们提出了几个简化属性，允许减少给定DRBD的结构。我们提供了HOL形式化的建议代数，并正式验证其相应的属性使用HOL4定理证明。这包括以可扩展的方式正式验证备用构造、串联、并联和更深层次结构的通用可靠性表达式，从而允许验证复杂系统的可靠性。最后，我们证明了这个代数的适用性，正式分析终端可靠性分析的洗牌交换网络在HOL4。
2019-08-06 cs.LO
Introducing Certified Compilation in Education by a Functional Language Approach
在计算机科学课程中，通常会有关于编译器技术的课程，内容涉及语法分析、语义分析、中间转换和目标代码生成等方面。本文介绍了通过函数语言的方法，在介绍过程中的编译器建设认证编译技术。针对在形式方法方面经验很少或没有经验的学生，证明过程使用Why3框架高度自动化。底层逻辑，语义建模和证明，连同练习和作业，导致了一个简单的命令式语言的正式验证编译器。本文涵盖了动机，课程设计，工具的选择，和教学方法，以及评价和建议的改进，从学生和教师的角度。
2019-06-27 cs.LO cs.PL
Formally Verified Approximate Policy Iteration
Technische Universität München（慕尼黑工业大学）；King’s College London（伦敦国王学院）
本文用 Isabelle/HOL 形式化验证因子 MDP 上的近似策略迭代算法，并将其精化为可执行实现，同时开发线性规划解认证软件以验证其实用性。
2024-06-11 cs.AI cs.LO
Plotting in a Formally Verified Way
计算机代数系统的一个非常宝贵的特性是它们能够绘制函数图。不幸的是，当人们试图设计一个数学函数库时，由于该用例固有的准确性问题，此功能通常会不足，产生不正确和潜在的误导性图。本文研究了情节正确的含义以及如何形式化地验证这一属性。Coq的证明助手，然后变成一个工具，用于绘制函数图使用可靠的多项式近似。此功能作为CoqInterval库的一部分提供。
2021-08-06 cs.LO cs.SE
VEL: A Formally Verified Reasoner for OWL2 EL Profile
Kansas State University（堪萨斯州立大学）
针对OWL推理器可靠性不足的问题，研究者开发了经形式化验证的EL++推理器VEL，基于Coq证明助手实现算法提取并修正了原算法的完备性缺陷，为高风险场景下的推理正确性提供了保障。
2024-12-11 cs.AI cs.LO cs.PL
Differential Testing of a Verification Framework for Compiler Optimizations (Experience Paper)
我们希望验证GraalVM编译器中优化阶段的正确性，该编译器由数千行执行复杂图形转换的复杂Java代码组成。我们已经建立了高层次的数据结构和操作的代码使用Isabelle/HOL定理证明器的模型，并可以正式验证这些高层次的操作的正确性。但剩下的挑战是：我们如何确保这些高级操作准确地反映Java正在做的事情？本文通过应用几种不同类型的差异测试来验证形式模型和Java代码具有相同的语义来解决这个问题。这些验证技术中的许多应该适用于其他正在构建真实代码的正式模型的项目。
2022-12-04 cs.LO cs.PL cs.SE
Verified Secure Compilation for Mixed-Sensitivity Concurrent Programs
该研究使用Isabelle/HOL验证了一个单遍编译器能够保持混合敏感并发程序的非干扰性，通过引入分解原则简化安全精化证明，并在真实用例上自动保留安全属性。
2022-02-28 cs.CR cs.LO cs.PL
A Formally Verified Lightning Network
本文利用 Why3 平台对闪电网络进行形式化验证，首次提供机器可检查的证明，证明其在所有场景下均能保护诚实用户资金安全。
2025-03-10 cs.CR cs.LO
Certified Knowledge Compilation with Application to Formally Verified Model Counting
针对知识编译输出缺乏正确性保证的问题，提出分区操作图（POGs）及CPOG证明框架，并开发基于D4的生成与验证工具链及Lean 4形式化验证的模型计数器，构成首个形式化验证的模型计数工具链。
2025-01-22 cs.LO
From Rocq to Metal: A Pipeline for Formally Verified Microcontroller Firmware
Ledger；Telecom Paris（巴黎电信学院）；Ledger Donjon
本文提出Encore!虚拟机，通过延续传递风格运行Rocq提取的Scheme代码，实现微控制器固件的形式化验证，并利用大语言模型辅助策略合成自动证明固件正确性。
2026-09-22 cs.LO cs.PL cs.SE
Composition Direction of Seymour's Theorem for Regular Matroids -- Formally Verified
本文在Lean 4中形式化验证了Seymour定理的正则拟阵组合方向，开发了相关矩阵与拟阵库，适用于有限秩且底集可能无限的情形。
2025-09-24 cs.LO math.CO
Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline
Ascendr, Inc.（Ascendr公司）
本文提出一种混合AI与Lean 4的正式验证框架，用于专利分析。通过依赖类型理论，实现了专利自由实施、权利主张敏感性、交叉权利主张一致性等五种知识产权应用场景的正式化验证，利用Lean 4进行机器验证，确保计算的数学正确性。
2026-04-20 cs.AI cs.LO cs.PL
COGENT: Certified Compilation for a Functional Systems Language
我们提出了一个自证明编译器的COGENT系统语言。COGENT是一种受限制的、多态的、高阶的、纯函数式的语言，具有线性类型，不需要可信的运行时或垃圾收集器。它编译成高效的C代码，旨在与现有的C函数互操作。该语言适用于具有最小共享的分层系统代码，例如文件系统或网络协议控制代码。对于类型良好的COGENT程序，编译器生成C代码，在Isabelle/HOL中对其语义进行高级浅嵌入，并证明C代码正确实现了此嵌入。其目的是让证明工程师能够高效地、均衡地推理真实世界系统代码的全部语义，同时保持C语言的互操作性和简洁性。我们描述了编译器的形式化验证阶段，其中包括自动化的形式化细化演算，从命令式更新语义到函数值语义的切换，以及一些标准的编译器阶段，如类型检查和单态化。编译器证书是一系列语言级的Meta证明和每个程序的翻译验证阶段，在Isabelle/HOL中组合成一个连贯的顶级定理。
2016-01-21 cs.LO cs.PL
Formally Verified Trades in Financial Markets
我们介绍了一个分析金融市场交易的正式框架。如今，所有大型交易所都使用计算机算法来匹配买入和卖出请求，这些算法必须遵守某些监管准则。例如，市场监管机构强制要求交易所产生的匹配应该是公平的、统一的和个体理性的。为了验证这些属性的行业，我们首先正式定义这些概念的定理证明，然后制定了许多重要的结果匹配的需求和供应。最后，我们使用这个框架来验证两类重要的双边拍卖机制的性质。本文中给出的所有定义和结果都在Coq证明助手中完全形式化，而不需要添加任何额外的公理。
2020-07-18 cs.DS cs.GT cs.LO
A Formalization of the Yul Language and Some Verified Yul Code Transformations
本文使用 ACL2 对 Solidity 编译器中间语言 Yul 的语法、语义及代码转换进行形式化，并证明静态与动态语义关系及转换正确性。
2025-07-25 cs.LO cs.PL
(Nearest) Neighbors You Can Rely On: Formally Verified k-d Tree Construction and Search in Coq
本文使用Coq证明助手形式化验证了k-d树的构建与K近邻搜索算法，提出了一种基于列表排列概念的直观方法来指定这些算法的属性。
2023-11-18 cs.CG cs.LO
Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces
本文提出一种基于张量语义的LTLf形式化方法，在Isabelle/HOL中验证正确性，并集成到神经符号学习中，通过可微损失函数实现约束训练，提供严谨且高效的框架。
2025-01-23 cs.AI cs.LG cs.LO
Creating a Formally Verified Neural Network for Autonomous Navigation: An Experience Report
Maynooth University（梅努斯大学）
本文通过案例研究探索了在自定义数据集上结合可微逻辑训练自主导航神经网络，使其通过设计满足安全属性，并总结了选择与使用神经网络验证器的经验。
2024-11-21 cs.CV cs.LG cs.LO
DRAFT: A Formally Verified Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments
Mathematical Sciences Institute, Australian National University（澳大利亚国立大学数学科学学院）；Faculty of Information Technology, Monash University（蒙纳士大学信息技术学院）
本文通过序数赋值形式化验证皮亚诺算术一致性的构造性证明，并使用Coq定理证明器验证所有结果。
2026-02-28 cs.LO
Proving the Coding Interview: A Benchmark for Formally Verified Code Generation
Beneficial AI Foundation（有益人工智能基金会）
本文引入最大形式化验证基准FVAPPS（含4715样本），将APPS的Python单元测试泛化为Lean 4未证明定理，测试显示Sonnet和Gemini证明正确率为30%和18%，挑战相关社区解决编程问题及正确性规范。
2025-02-08 cs.AI cs.LG cs.LO
CLEVER: A Curated Benchmark for Formally Verified Code Generation
UT Austin（得克萨斯大学）；Amazon（亚马逊）；Caltech（加州理工学院）
CLEVER是一个包含161个问题的精选基准，用于Lean中端到端验证代码生成，通过避免测试用例监督和规范泄露，评估少样本与智能体方法，发现现有方法难以完全验证，成为程序合成与形式推理的前沿挑战基准。
2025-10-23 cs.AI cs.LG cs.LO
A Formally Verified HOL4 Algebra for Event Trees
事件树（ET）分析作为一种前向演绎安全分析技术，在关键系统设计阶段被广泛用于决策。ET是表示系统中所有可能的操作状态和外部事件的示意图，以便这些可能的场景之一可能发生。在这份报告中，我们建议使用HOL 4定理证明的形式化建模和步骤分析的ET图。为此，我们在高阶逻辑中开发了一种基于通用列表数据类型的ET图的形式化，该数据类型可以：（i）构建任意级别的ET图;（ii）减少不相关的ET分支;（iii）划分ET路径;以及（iv）基于某些事件的发生进行概率分析。为了说明的目的，我们进行正式的ET逐步分析的电网，并确定其系统平均中断频率指数（SAIFI），这是一个重要的指标，系统的可靠性。
2020-04-29 cs.LO cs.SY eess.SY
Are Users More Willing to Use Formally Verified Password Managers?
本研究通过两项实验（15人形成性研究及200人定量研究）探究用户对形式化验证密码管理器的态度，发现用户视其为可取，并提出三项沟通改进建议。
2025-09-07 cs.CR cs.HC cs.LO
Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems
UC Berkeley（伯克利大学）；Google（谷歌）；UC Santa Cruz（圣克鲁兹大学）
提出归纳演绎合成（IDS）方法，通过联合增量合成实现与证明，并利用失败尝试学习，使AI在分布式系统规范上实现100%验证成功率，成本和时间远低于专家和现有AI代理。
2026-05-22 cs.AI cs.DC cs.LO
Dynamic Fault Trees Analysis using an Integration of Theorem Proving and Model Checking
动态故障树（DFTs）已成为一个重要的工具，捕捉系统故障的动态行为。然后，这些DFT定性和定量分析，使用随机或代数方法来判断给定系统的故障特征的子组件的故障。模型检验最近已被提出来进行故障分析的系统使用DFT的动机，以提供一个严格的故障分析的安全关键系统。然而，模型检验还没有被用于DFT的定性分析和约简算法中使用的模型检验通常没有正式验证。而且，分析时间随着状态数的增加呈指数增长。这些问题限制了模型检验在分析安全关键领域中使用的复杂系统时的有用性，在安全关键领域中，分析的准确性和完整性是最重要的。为了克服这些局限性，我们提出了一个全面的方法来进行定性和定量分析的DFT定理证明和模型检验为基础的方法集成。为此，我们形式化的所有基本的动态故障树门使用高阶逻辑的代数方法的基础上，并正式验证了一些简化属性。这种形式化允许我们使用定理证明器正式验证原始DFT和缩减DFT之间的等价性，并进行定性分析。然后，我们使用模型检验进行定量分析的正式验证减少DFT。我们应用我们的方法，以五个基准和结果表明，正式验证减少DFT分析使用模型检验与多达6倍少的状态和高达133000倍的速度。
2017-12-07 cs.LO
Vero: Can AI Agents Build Formally Verified Software Repositories?
University of Chicago（芝加哥大学）；California Institute of Technology（加州理工学院）；Stanford University（斯坦福大学）；UC Berkeley（加州大学伯克利分校）；Amazon Web Services（亚马逊云计算服务）；Apodex
研究推出首个仓库级验证软件综合基准Vero，含43个多模块实例，评估发现前沿智能体仅解决27个实例，为相关研究提供测试平台。
2026-08-14 cs.AI cs.LG cs.LO
A Revised and Verified Proof of the Scalable Commutativity Rule
本文解释了可扩展交换性规则（SCR）的公开证明中的一个缺陷，在Coq证明助手中给出了SCR的修改和正式验证的证明，并讨论了我们证明SCR的经验中提出的见解和开放性问题。
2018-09-23 cs.DC cs.LO
Phoenix: A Formally Verified Regenerating Vault
获得加密货币用户私钥访问权限的攻击者可以代替她执行任何操作。由于大多数加密货币的分散性，没有实体可以恢复这些操作。这是去中心化系统面临的一个核心挑战，许多引人注目的抢劫案就说明了这一点。保险库合同通过引入人为的操作延迟来降低这种风险，允许合同所有者在延迟期间流产。然而，钥匙被盗仍然使金库无法使用，并使资金处于危险之中。我们介绍凤凰，一种新颖的合同体系结构，允许用户恢复其安全属性后，密钥丢失。Phoenix利用用户将密钥存储在容易获得但不太安全的存储（第二层）以及更安全但更难访问的存储（第一层）中的能力。与以前的解决方案不同，用户可以在第二层密钥被盗后恢复Phoenix安全性，并且即使在任何一层中丢失密钥也不会丢失资金。Phoenix还引入了一种机制，以减少攻击者在第一层妥协的情况下可能造成的损害。我们正式指定了Phoenix所需的行为，并提供了Phoenix作为以太坊合约的原型实现。由于这样的实现是高度敏感的，容易受到微妙的错误，我们应用形式化验证工具来证明特定的代码属性和识别故障。我们强调了该工具识别的一个错误，该错误可能被攻击者利用来危害Phoenix。在修复缺陷后，该工具证明了底层可执行代码的正确性。
2021-06-02 cs.CR cs.LO
Verified Real Number Calculations: A Library for Interval Arithmetic
在机械证明中，初等函数的实数计算是非常困难的。在本文中，我们将展示如何在一个定理证明器或证明助手中以一种方便、高度自动化和交互式的方式进行这些计算。首先，我们正式建立了初等函数的上界和下界。然后，基于这些界限，我们开发了一个合理的区间算术实数计算发生在代数设置。为了减少区间算术的依赖效应，我们结合了两种技术：区间分裂和泰勒级数展开。这种务实的方法已经开发，并正式验证，在定理证明。正式的开发还包括一组可定制的策略，以自动化涉及实数显式计算的证明。我们的最终目标是提供有保证的数值性质的证明与最小的人类定理证明者的相互作用。
2007-08-28 cs.LO cs.MS
LeanBET: Formally-verified surface area calculations in Lean
University of Maryland, Baltimore County（马里兰大学巴尔的摩分校）
本文在Lean4中实现并验证了BET方法的完整流程，包括窗口枚举、单调性检查、膝点选择和线性回归，证明了算法的正确性并验证了与BETSI参考方法的一致性。
2026-05-15 cs.LO cs.MS physics.chem-ph
Formally Verified Animation for RoboChart using Interaction Trees
本文使用交互树为RoboChart提供操作语义，在Isabelle中实现并生成可执行动画，通过化学探测器和巡逻机器人案例验证了动画场景是CSP指称语义的迹细化，确保了方法的正确性。
2023-09-13 cs.LO
Formally Verified Liveness with Multiparty Session Types in Rocq
University of Edinburgh（爱丁堡大学）；University of Oxford（牛津大学）；School of Computer Science and Engineering, University of New South Wales（新南威尔士大学计算机科学与工程学）
本文在Rocq证明助手中首次机械化证明了同步多方会话类型的活性，利用共归纳树和子类型关系建立局部类型与全局类型的操作对应，从而保证会话的安全性和活性。
2026-05-22 cs.LO
Verifying Verified Code
Chong等人最近在AWS的一个案例研究中提出了一种有效的工业界有界模型检验方法。在本文中，我们报告了一个后续的案例研究，从三个研究问题的角度探讨了方法：（a）证明工件可以跨验证工具使用;（b）验证代码中是否存在错误;（c）规范是否可以改进。为了研究这些问题，我们将$\texttt{aws-c-common}$库的验证任务移植到SEAHORN和KLEE。我们展示了使用编译器语义和交叉检查规范与不同的验证技术的好处，并呼吁标准化证明库扩展，以增加规范的重用。讨论的核查任务可在网上公开查阅。
2021-07-01 cs.LO cs.SE
Formally Verified Next-Generation Airborne Collision Avoidance Games in ACAS X
飞机防撞算法的设计是一个微妙但重要的挑战，值得证明安全保证的需要。考虑到入侵飞机决策、本机驾驶员反应和飞机连续运动动力学的微妙性之间的相互作用的不可预测性，获得这样的保证是不平凡的。现有的防撞系统，如TCAS和下一代机载防撞系统ACAS X，已经被分析为假设对入侵者的飞行机动有严格的限制，限制了它们在入侵者可能改变航向的真实场景中的安全保证。这项工作需要一个概念上的显着和实际相关的偏离现有的ACAS X模型，将它们推广到混合游戏与一流的代表性的所有权和入侵者的决定来自两个独立的球员，使显着先进的预测能力。通过证明微分博弈逻辑中的对抗性ACAS X的获胜策略的存在性，建立了本机和入侵者飞机的丰富遭遇的碰撞自由，沿着具有不断变化的垂直/水平速度的飞行路径的微分方程具有独立的决策。我们提出了三种类型的模型的复杂性不断增加：单咨询无限时间模型，有界时间模型，无限时间，多咨询模型。在每一类模型中，我们确定象征性的条件，并证明，然后总是有一个可能的本机机动，将防止两架飞机之间的碰撞。
2022-03-01 cs.GT cs.LO cs.SY
Towards a Coq-verified Chain of Esterel Semantics
本文利用 Coq 构建并验证 Esterel 的形式语义链，提出去除 Must/Can 势函数对的微步语义，并证明其对 CSS 的精化以及 CBS 与 CSS 的等价性。
2025-01-06 cs.FL cs.LO cs.PL
Proving soundness of combinatorial Vickrey auctions and generating verified executable code
使用机械化的推理，我们证明了组合Vickrey拍卖是健全的规定，他们将一个独特的结果（分配和转让）的任何有效的输入（出价）。这样做之后，我们从正式定义的拍卖中自动生成经过验证的可执行代码。这消除了在实现拍卖设计中的错误来源。我们打算使用正式的方法来验证新的拍卖设计。在这里，我们的贡献是介绍和展示使用正式的方法进行拍卖验证在熟悉的设置一个著名的拍卖。
2013-09-02 cs.CE cs.GT cs.LO
Pursuit of Truth and Beauty in Lean 4: Formally Verified Theory of Grammars, Optimization, Matroids
Institute of Science and Technology Austria（奥地利科学技术学院）
本文通过形式化验证探讨数学中的语法理论、优化与Matroid理论，旨在创建可理解、可信、有用且优雅的代码，强调定义的可读性和可信度，而非易于操作的定义。
2026-03-25 cs.LO math.HO
Fundamental Limits in Formal Verification of Message-Passing Neural Networks
University of Kassel（卡塞尔大学）
输出可达性和对抗鲁棒性是神经网络最相关的安全属性之一。我们表明，在消息传递神经网络（MPNN）的背景下，一个常见的图神经网络（GNN）模型，形式化验证是不可能的。特别是，我们表明，输出可达的图分类MPNN，工作在图的无界大小，非平凡程度和充分表达节点标签，不能正式验证：有没有算法，正确回答（是或否），给定一个MPNN，是否存在一些有效的输入MPNN，使相应的输出满足给定的规格。然而，我们也表明，输出的可达性和对抗性的鲁棒性节点分类MPNN可以正式验证时，输入图的程度的限制是先验的。我们讨论了这些结果的影响，为了获得一个完整的图片的原则可能性，正式验证GNN，根据所涉及的GNN模型和输入输出规格的表现力。
2022-10-04 cs.LG cs.LO
Bit-Vector Abstractions to Formally Verify Quantum Error Detection & Entanglement
North Dakota State University（北达科他州立大学）
本文提出位向量抽象方法用于验证量子电路，有效分离叠加与功能行为，验证了2-3-9量子码错误检测电路、贝尔态和GHZ态生成电路，展示了方法的高效性和可扩展性。
2026-03-29 cs.ET cs.LO quant-ph
