On Integrating Deductive Synthesis and Verification Systems
我们描述了在无界域上的递归函数程序的合成和验证技术。我们的技术建立在可满足性模递归函数的算法之上，演绎合成的框架，以及代数数据类型的完整合成过程。我们提出了新的反例引导算法构造验证程序。我们已经实现了这些算法在一个集成的环境中进行交互式验证和合成关系规范。我们的系统能够合成一些有用的递归函数，操作无界的数字和数据结构。
2013-04-20 cs.LO cs.PL cs.SE
A Deductive Verification Framework For Higher Order Programs
在本报告中，我们介绍了为我们的APDC（Area Prática de Desenvolvimento Curriculum）课程研究项目开展的初步工作。这个项目的主要目标是开发一个框架，在Why3工具之上，用于验证有效的高阶程序。我们使用去功能化作为从高阶OCaml实现到一阶OCaml实现的中间转换。我们翻译的目标是WhyML，Why3的程序设计语言。我们相信去功能化可以是一个有趣的路线，高阶程序的自动验证，因为人们可以采用现成的自动程序验证器来证明所生成的一阶程序的正确性。这份报告还向读者介绍了演绎程序验证的主题，以及用于证明高阶有效程序的一些工具和概念。
2020-11-28 cs.LO cs.PL
VeGo: Direct Deductive Formal Verification of Go Programs for Computer Science Education
University of Saskatchewan（萨斯喀彻温大学）
该研究提出面向计算机科学教育的VeGo系统，可直接验证标准Go程序，整合多种形式化验证技术，对比其他语言论证Go的优势，经教育教材评估并规划了形式并发规约的路线图。
2026-08-25 cs.PL
Caesar: A Deductive Verifier for Probabilistic Programs
RWTH Aachen University（亚琛工业大学）；Cornell University（康奈尔大学）；Saarland University（萨尔兰大学）；University College London（伦敦大学学院）；DTU Compute（丹麦技术大学计算系）；University of Oldenburg（奥尔登堡大学）
Caesar通过HeyVL语言实现概率程序的验证，支持自定义证明规则和模型检查后端，具备五年研发成果与改进功能。
2026-05-15 cs.PL
Automated Deductive Verification for Ladder Programming
梯形图逻辑是IEC 61131-3标准化的程序设计语言，广泛用于对工业可编程逻辑控制器（PLC）进行编程。PLC程序由输入（其值在运行时由工厂传感器给出），输出（其值在运行时提供给工厂执行器）和从输入值计算输出值的逻辑表达式组成。由于梯形图程序的图形形式，以及典型工业程序中的输入和输出量，调试此类程序既耗时又容易出错。在本文中，我们提出了一个基于Why 3的工具原型，我们已经实现了自动化的演绎验证的使用，以提供一个易于使用和强大的调试工具的阶梯程序员。
2019-12-23 cs.LO cs.PL cs.SE
HaliVer: Deductive Verification and Scheduling Languages Join Forces
本文提出 HaliVer，将演绎验证器 Vercors 集成到 Halide 中，用同一规约验证算法及其调度生成的并行优化代码，显著减少标注并证明内存安全与功能正确性。
2024-01-19 cs.LO cs.PL
Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis
University of California, Berkeley（加州大学伯克利分校）
即使在自动化的形式化方法令人印象深刻的进步，在系统验证和综合的某些问题仍然具有挑战性。例子包括验证软件的定量属性，包括对时间和能量消耗的约束，以及从规范中自动合成系统。主要的挑战包括环境建模、规范的不完整性以及底层决策问题的复杂性。本文提出了一种通过整合归纳推理、演绎推理和结构假设来应对这些挑战的方法。演绎推理，从一般规则或概念导出关于特定问题实例的结论，包括逻辑推理和约束求解等技术。归纳推理，从特定的实例中概括出一个概念，包括从例子中学习算法。结构假设用于定义工件的类别，例如在验证或合成过程中生成的不变量或程序片段。演绎使用结构假设来约束归纳和演绎推理，并积极地结合归纳和演绎推理：例如，演绎技术生成用于学习的示例，并且归纳推理用于指导演绎引擎。我们用三个应用来说明这种方法：（i）软件的时序分析;（ii）无循环程序的合成，以及（iii）混合系统的控制器合成。一些未来的应用进行了讨论。
2012-01-04 cs.AI cs.LO cs.PL
RHLE: Modular Deductive Verification of Relational $\forall\exists$ Properties
Hoare风格的程序逻辑是一种流行而有效的软件验证技术。关系程序逻辑是这种方法的一个实例，它能够推理两个或多个程序执行之间的关系。现有的关系程序逻辑集中于验证程序集合的所有运行不违反指定的关系行为。几个重要的关系属性，包括精细化和不干涉，不属于这一类别，因为它们也要求存在特定的理想执行。本文介绍了RHLE，用于验证这些类型的关系$\forall\exists$属性的逻辑。我们的方法的关键是一种新形式的函数规范，采用了一个变种的幽灵变量，以确保有效的实现表现出某些行为。我们已经使用了一个基于RHLE的程序验证器来验证一组不同的关系$\forall\exists$属性从文献中得出。
2022-09-08 cs.LO cs.PL
Deductive Verification of Parallel Programs Using Why3
消息传递接口规范（MPI）定义了一个用于并行计算机编程的可移植消息传递API。MPI程序在正确性方面存在许多挑战：通信中的发送值和期望值可能不匹配，导致不正确的计算，可能导致崩溃;程序可能会死锁，导致资源浪费。现有的工具是不完全令人满意的：模型检查不规模与过程的数量，测试技术浪费资源，并高度依赖于测试集的质量。作为一种替代方案，我们提出了一个原型的基于类型的方法来编程和验证MPI像程序对协议。协议是用依赖类型语言编写的，旨在捕获MPI中最常见的原语，此外还包含一种原语递归和集体选择的形式。然后将协议翻译成Why 3，一种演绎软件验证工具。而源代码则是用Why 3平台的语言WhyML编写的，并根据协议进行检查。保证通过验证的程序是通信安全的，没有死锁。我们使用我们的方法验证了教科书中的几个并行程序，并报告了结果。
2015-08-20 cs.DC cs.PL
Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
本文为含循环、连续分布和条件化的概率程序验证奠定基础，通过黎曼和近似积分实现SMT不变量验证，并证明收敛性与完备性，且可在现有工具中应用。
2025-02-26 cs.LO cs.PL
Deductive Verification of Programs with Underspecified Semantics by Model Extraction
本文提出了一种新的、自动化程度高的语义欠规范程序的形式化验证方法，一种语言语义学，它不确定某些求值的顺序。首先，我们减少这个问题的非确定性的分布式系统，自动提取一个分布式的主动对象模型，欠指定的，顺序的C代码。这个翻译过程为所考虑的C子集提供了一个完全正式的语义。在所提取的模型中，每个非确定性选择对应于一个可能的评估顺序。此步骤还自动将ANSI/ISO C规约语言（ACSL）中的规范转换为活动对象的方法契约和对象不变量。然后，我们对指定的Active Objects模型执行验证。为此，我们已经实现了一个定理证明器Crowbar的基础上的行为程序逻辑（BPL），它验证了提取的模型相对于翻译的规范，并确保原始属性的C代码的所有可能的评估订单。通过使用模型提取，我们可以使用标准的工具，而不需要设计一个新的复杂的程序逻辑来处理欠规格说明。所使用的案例研究是高度低估，不能用现有的C语言工具进行验证。
2022-02-11 cs.LO cs.PL
Scalable Probabilistic Program Verification via Typed Extended Decision Diagrams
RWTH Aachen University（亚琛工业大学）；Cornell University（康奈尔大学）；Radboud University（拉德堡德大学）
针对概率程序验证中弱前置期望表示爆炸问题，提出类型化扩展决策图（TEDD）表示和SMT剪枝方法，将可扩展性提升数个数量级。
2026-06-24 cs.PL
Towards deductive verification of MPI programs against session types
消息传递接口（MPI）是开发并行应用程序的事实标准消息传递基础设施。在第一版库规范发布20年后，基于MPI的应用程序现在通常部署在超级计算机和集群计算机上。这些用C或Fortran编写的应用程序表现出复杂的消息传递行为，因此很难静态验证重要属性，例如不存在死锁。我们的工作建立在会话类型，一个理论描述协议，在这方面提供正确的建设保证。我们注释MPI原语和C代码与会话类型的合同，写在语言的软件验证C。然后用软件验证器检查带注释的代码的正确性。我们提出了初步的结果，并讨论了未来的挑战，验证现实的MPI程序符合会话类型。
2013-12-10 cs.DC cs.LO cs.PL
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
针对演绎验证中可满足含量词公式仅有无限模型、现有求解器只能找有限反例且易发散的问题，提出符号结构、符号模型搜索过程及涵盖多种类 EPR 的新可判定片段。
2024-09-10 cs.LO cs.PL
Teaching Design by Contract using Snap!
随着演绎程序验证研究的进展，新的工具和技术已成为可用于支持契约式设计推理的非平凡程序编写的广泛使用的程序设计语言。然而，演绎程序验证仍然是专家的活动，在编程，规范和验证方面有丰富的经验。我们想改变这种情况，通过开发程序验证技术，可用于更大的观众。在本文中，我们介绍了我们如何开发原型程序验证支持Snap！啪！是一种可视化的程序设计语言，特别针对高中生。我们以类似的视觉风格添加了规约语言构造，旨在使预期的语义从规范构造的外观和感觉中变得清晰。我们提供Snap的静态和动态验证支持！程序.特别注意错误消息，使其尽可能直观。
2021-07-12 cs.PL cs.SE
Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)
RWTH Aachen University（亚琛工业大学）
本文提出通过切片技术提升概率程序验证的诊断能力，通过Brutus实现高效错误定位与验证提示。
2025-12-24 cs.PL
Gradually Verifying Unfolding Expressions & Pure Functions
Clemson University（克莱姆森大学）；Carnegie Mellon University（卡内基梅隆大学）；ETH Zürich（苏黎世联邦理工学院）；Purdue University（普渡大学）
本文针对使用符号执行的验证器，给出展开表达式和纯函数的形式语义并扩展到渐进验证器，提供健全性证明，支持Gradual C0，结果也适用于相关静态验证器，以此提高涉及所有权规范的模块化。
2026-07-20 cs.PL
Deductive Proof of Ethereum Smart Contracts Using Why3
bug或错误是任何软件或计算机程序都可能遇到的常见问题。这可能是由于程序编写不当、键入错误或存储管理不当造成的。然而，如果不安全的程序用于关键系统，错误可能成为一个重大问题。因此，这类系统的形式化方法是非常必要的。在本文中，我们使用一种形式语言，对基于智能合约的以太坊区块链应用程序进行演绎验证，智能合约是自动执行的数字合约。区块链系统操纵加密货币和交易信息。因此，如果区块链中发生错误，可能会发生严重的后果，例如金钱损失。因此，本文的目的是提出一种专门用于演绎验证的语言，称为Why 3，作为编写正式和验证智能合约的新语言，从而避免利用此类合约执行漏洞的攻击。我们首先编写Why 3智能合约程序;接下来我们制定规范以证明不存在运行时错误属性和函数属性，然后我们使用Why 3系统验证程序的行为。最后，我们将Why 3合约编译到以太坊虚拟机（EVM）。此外，我们给出了一组通用的数学语句，可以验证适合任何类型的持有加密货币的智能合约的功能属性，这表明Why 3可以成为编写智能合约的合适语言。为了说明我们的方法，我们描述了其应用到一个现实的工业用例。
2019-08-23 cs.LO cs.PL
Gobra: Modular Specification and Verification of Go Programs (extended version)
Go是一种越来越流行的系统程序设计语言，特别是针对并发和分布式系统。Go语言与其他命令式语言的不同之处在于，它通过goroutine提供了结构化的子类型和轻量级的并发性以及消息传递通信。这些特性的组合为静态验证提出了有趣的挑战，最突出的是可变堆和高级并发原语的组合。我们提出Gobra，一个模块化的，演绎的程序验证器，证明内存安全，崩溃安全，数据竞争自由，和用户提供的规范。Gobra基于分离逻辑，支持Go语言的一个大子集。它的实现将带注释的Go程序转换为Viper中间验证语言，并使用现有的基于SMT的验证后端来计算和履行证明义务。
2021-05-28 cs.PL
A Complete, Formal Semantics for Rust Source Code
Technical University of Darmstadt（达姆施塔特工业大学）
本文提出一种基于局部抽象、全局具体框架的模块化 Rust 形式化语义，支持异步特性与 Tokio，并证明调度器公平性及程序逻辑可靠性。
2026-10-06 cs.PL
Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml
本文提出一种针对 OCaml 高阶迭代器的通用规约与演绎验证方法，利用 Gospel 语言描述迭代行为并通过 Cameleer 框架验证客户端正确性，经列表与图算法案例验证有效。
2025-06-25 cs.LO cs.PL
Experience Report on Formally Verifying Parts of OpenJDK's API with KeY
软件的演绎验证尚未进入行业，因为复杂性和可扩展性问题需要高度专业的专家。然而，长期的观点是开发验证工具，帮助工业软件开发人员更快，更容易地找到软件系统中的错误或瓶颈。KeY项目构成了一个用于指定和验证软件系统的框架，旨在使形式化验证工具适用于主流软件开发。为了帮助KeY的开发人员、用户和演绎验证社区，我们从用户的角度总结了使用KeY 2.6.1指定和验证真实世界Java代码的经验。为此，我们集中讨论OpenJDK 6的Collections-API的部分内容，其中存在非正式规范。当我们描述我们如何桥接非正式和正式规范时，我们也展示了我们遇到的伴随的挑战。我们的经验是，（a）原则上，演绎验证类API代码库是可行的，但需要很高的专业知识，（b）为现有的代码库开发正式的规范仍然是出了名的困难，（c）在Java中的某些语言结构的规格是具有挑战性的工具建设者。我们在指定OpenJDK 6的部分方面的初步努力构成了未来研究案例研究的垫脚石。
2018-11-27 cs.LO cs.PL cs.SE
Towards Automated Verification of LLM-Synthesized C Programs
本文提出 \synver{} 框架，通过对 LLM 生成的 C 程序施加语法与语义偏置，并基于 Verified Software Toolchain 构建验证工具，实现程序合成与自动化验证。
2025-10-20 cs.PL
Lightweight Interactive Proving inside an Automatic Program Verifier
在形式化方法中，演绎验证方法允许在关键软件上建立最强可能的形式化保证。缺点是设计适当的正式规范和成功履行所需的证明义务所需的人力成本。为了在工业软件开发环境中推广演绎验证，必须提供从简单和自动化方法逐步过渡到演绎验证的方法。SPARK环境，用于开发用Ada编写的关键软件，通过提供自动化工具来正式证明某些代码满足Ada合同中表达的要求，从而实现了这一目标。在利用自动证明器来履行证明义务的程序验证器中，需要一些额外的用户与证明任务的交互：或者帮助分析证明失败的原因，或者最终履行最先进的自动证明器无法达到的验证条件。在SPARK中添加交互式证明功能似乎很复杂，因为证明工具链使用了独立的中间验证工具Why 3，它足够通用，可以接受不同输入语言的多个前端。本文报告了我们的方法来扩展Why 3与交互式证明功能，并与一个通用的客户端-服务器基础设施，允许集成到一个外部的，前端的图形用户界面，如SPARK的证明交互。
2018-11-27 cs.LO cs.PL cs.SE
RustyDL: A Program Logic for Rust
Technische Universität Darmstadt（达姆施塔特工业大学）
RustyDL 是一种针对 Rust 的程序逻辑，旨在为自动交互式演绎验证工具提供基础，通过源代码级别推导提升复杂功能属性的验证能力。
2026-02-25 cs.LO cs.PL
InvWeaver: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs
Nanjing University（南京大学）；Hunan University（湖南大学）；Birkbeck, University of London（伦敦大学伯贝克学院）
研究针对交互循环程序的不变式合成难题，提出神经符号框架InvWeaver，通过循环级抽象等方法揭示循环间依赖并传播证明义务，在综合基准套件上评估，其性能显著优于现有方法，能有效解决多循环问题并保持单循环任务优势。
2026-07-08 cs.LG cs.PL
Reasoning about Iteration and Recursion Uniformly based on Big-step Semantics
可靠的演绎程序验证技术应该被证明是相对于程序设计语言的语义合理的。对于每一种不同的语言，构造一个单独的可靠性证明往往是一项艰巨的任务。在独立于语言的程序验证中，讨论了计算机程序的共同方面，以使所有语言都能进行合理的推理。在这项工作中，我们提出了一个解决方案，合理的推理迭代和递归的基础上的大步骤操作语义的任何程序设计语言。我们给出了我们的推理技术的合理性和相对完整性的归纳证明。我们说明了在简化的程序设计语言的命令式和功能的范例，具有不同的功能的技术。我们还在Coq证明助手中机制化所有正式结果。
2021-08-04 cs.PL
Solver-Aided Constant-Time Circuit Verification
我们提出了氙，求解器辅助的方法，正式验证Verilog硬件在恒定时间执行。Xenon通过一种新的恒定时间反例概念，大大减少了定位验证失败根本原因所需的工作量，从而扩展到实际的硬件设计，Xenon使用该反例自动合成一组最小的保密假设。Xenon通过模块摘要的概念进一步利用Verilog代码中的模块性，从而避免多个模块实例化之间的重复工作。我们展示了氙的假设合成和总结如何使各种电路的验证，包括AES，高度模块化的AES-256实现，其中模块化将验证从6小时减少到3秒以下，以及ScarV，一种时序通道硬化的RISC-V微控制器，其大小超过以前验证的设计一个数量级。
2021-04-01 cs.CR cs.PL
CISE3: Verificação de aplicações com consistência fraca em Why3
在这篇文章中，我们提出了一个工具，用于验证建立在顶级复制数据库上的程序。该工具评估顺序规范，并推断哪些操作需要同步，以便程序在分布式环境中正常运行。我们的原型是建立在演绎验证平台Why3。Why3框架提供了一个复杂的用户体验，扩展到现实案例研究的可能性，以及高度的自动化。一个案例研究和讨论，实验验证我们的方法的目的。
2019-09-09 cs.LO cs.PL
QWIRE Practice: Formal Verification of Quantum Circuits in Coq
我们描述了在Coq证明助手中嵌入QWIRE量子电路语言。这允许程序员使用高级抽象来编写量子电路，并使用Coq的定理证明功能来证明这些电路的属性。该实现使用高阶抽象语法来表示变量绑定，并为线性导线类型提供类型检查算法，确保量子电路是良构的。我们形式化了一个指称语义，将QWIRE电路解释为密度矩阵上的超算子，并证明了一些简单量子程序的正确性。
2018-03-02 cs.ET cs.LO cs.PL
Verification of Recursively Defined Quantum Circuits
本文提出一个用于验证递归定义量子电路正确性的证明系统，并证明其可靠性与相对完备性，通过多个应用实例展示了其有效性。
2024-11-06 cs.LO cs.PL quant-ph
Giallar: Push-Button Verification for the Qiskit Quantum Compiler
本文介绍了Gialar，量子编译器的全自动验证工具包。Gialar不需要手动规范、不变量或证明，并且可以自动验证编译器是否保留了量子电路的语义。为了处理量子编译器中的无界循环，Gialar抽象了三个循环模板，其循环不变量可以自动推断。为了有效地检验具有复杂矩阵语义表示的任意输入和输出电路的等价性，Gialar引入了量子电路的符号表示和一组表示符号量子电路等价性的重写规则.使用Gialar，我们在Qiskit编译器（开源量子编译器标准）的13个版本中实现并验证了44个（共56个）编译器通道，在此期间，Qiskit检测到并确认了三个错误。我们的评估表明，大多数Qiskit编译器通过可以在几秒钟内自动验证，验证只会对编译性能产生适度的开销。
2022-05-02 cs.PL quant-ph
Verifying C11-Style Weak Memory Libraries
演绎验证的并发程序在弱内存下，到目前为止，仅限于简单的程序在一个单一的状态空间。对于可伸缩性，我们还需要具有可验证库抽象的模块化技术。本文解决了这一挑战的背景下，RC 11 RAR，C11内存模型的一个子集，允许放松和释放获取访问，但不允许，所谓的负载缓冲周期。我们开发了一个简单的框架，用于指定抽象对象，精确地描述了抽象方法调用的可观察性保证。我们展示了如何将这个框架与一个操作语义集成，该操作语义使客户端程序执行它使用的库中的抽象方法调用的验证成为可能。最后，我们将展示如何实现这样的抽象在RC 11 RAR可以验证通过开发一个（上下文）细化框架的抽象对象。我们的框架，包括操作语义，客户端库程序的验证技术，和抽象库和它们的实现之间的模拟，已在伊莎贝尔/HOL机械化。
2020-12-28 cs.LO cs.PL
Formal Verification of Variational Quantum Circuits
University of Verona（维罗纳大学）
本文首次对变分量子电路（VQCs）的形式化验证问题展开深入研究，提出基于抽象解释的新型语义框架以克服量子状态归一化带来的变量依赖挑战，并在标准基准上验证了该方法的有效性。
2025-07-14 cs.LG cs.PL quant-ph
Verifying C11-Style Weak Memory Libraries via Refinement
演绎验证的并发程序在弱内存下，到目前为止，仅限于简单的程序在一个单一的状态空间。对于可伸缩性，我们还需要具有可验证库抽象的模块化技术。本文解决了这一挑战的背景下，RC 11 RAR，C11内存模型的一个子集，允许放松和释放获取访问，但不允许，所谓的，负载缓冲周期。我们开发了一个简单的框架，用于指定抽象对象，精确地描述了抽象方法调用的可观察性保证。我们展示了如何将这个框架与一个操作语义集成在一起，该操作语义可以验证客户端程序从他们使用的库中执行抽象方法调用。最后，我们将展示如何实现这样的抽象在RC 11 RAR可以验证通过开发一个（上下文）细化框架的抽象对象。我们的框架，包括操作语义，客户端库程序的验证技术，和抽象库和它们的实现之间的模拟，已在伊莎贝尔/HOL机械化。
2021-08-16 cs.LO cs.PL
Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics
容错分布式协议的验证是一项非常困难的任务。通常，在这些协议中，在过程代码和其正确性证明中都使用关于集合基数的阈值，例如，进程仅在其已从至少一半的对等体接收到确认时才可执行动作。基于阈值的协议的验证是非常具有挑战性的，因为它涉及两种推理：关于协议的无界状态的一阶推理，以及关于集合和基数的推理。在这项工作中，我们开发了一种新的方法，用于将此类协议的验证任务分解为两个可判定的逻辑：EPR和BAPA。我们的关键见解是，这样的协议使用阈值在一个有限的方式作为一种手段，以获得某些属性的“交集”之间的集合。我们定义了一种语言来表达这样的属性，并提出了两个翻译：EPR和BAPA。EPR转换允许验证协议，同时假设这些属性，BAPA转换允许验证属性的正确性。我们进一步开发了一种算法，用于自动生成验证给定协议所需的属性，便于全自动演绎验证。使用这种技术，我们已经验证了几个具有挑战性的协议，包括拜占庭一步共识，混合可靠广播和快速拜占庭Paxos。
2019-05-19 cs.DC cs.LO cs.PL
CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler
我们提出了CertiQ，一个验证框架，用于编写和验证Qiskit，最广泛使用的量子编译器的编译器通行证。据我们所知，CertiQ是第一个以最自动化的方式验证真实世界量子编译器通过的努力。在CertiQ接口中编写的带有注释的验证器通道可用于生成验证条件，以及可集成到Qiskit中的可执行代码。CertiQ引入了量子电路演算，通过将这种检查过程编码到SMT问题中来实现量子线路的等效性的有效检查。CertiQ还提供了一个经过验证的广泛使用的数据结构库、电路转换函数以及不同量子数据表示的转换函数。这个经过验证的库不仅可以进行模块化验证，而且还可以为未来的量子编译器设计提供指导。我们已经在CertiQ中重新实现并验证了26个（共30个）Qiskit编译器通道，在此期间，在Qiskit实现中检测到三个错误。我们验证的编译器通过实现通过了所有Qiskit的回归测试，没有显示出明显的性能损失。
2020-11-26 cs.ET cs.PL quant-ph
