Deductive Verification of Weak Memory Programs with View-based Protocols (extended version)
University of Twente（特温特大学）；TU Delft（代尔夫特理工大学）；Eindhoven University of Technology（埃因霍温理工大学）
本文提出在VerCors中编码弱内存并发的方案，通过扩展原子操作支持并引入协议自动机概念，实现基于许可的分离逻辑，用于验证弱内存并发程序的正确性。
2026-04-22 cs.LO
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
Cameleer: a Deductive Verification Tool for OCaml (extended version)
OCaml特别适合于形式化验证。一方面，它是一种具有良好定义的语义的多范式语言，允许编写干净，简洁，类型安全和高效的代码。另一方面，它是实现合理软件的首选语言，例如，工业编译器、证明助手和自动求解器。然而，除了一些交互式工具之外，形式化验证很少应用于OCaml编写的程序。在本文中，我们介绍了正在进行的项目Cameleer，旨在为OCaml开发一个演绎验证工具，重点是证明自动化。我们利用最近提出的GOSPEL，通用OCaml SPE规范化语言，附加严格的，但可读的，行为规范的OCaml代码。正式指定的程序被馈送到我们的工具链，该工具链将其转换为WhyML中的等效程序，WhyML是Why3验证框架的编程和规约语言。最后，Why3是用来计算验证条件所产生的程序，它可以由现成的SMT求解器放电。我们提出了成功的应用程序的Cameleer工具，以证明功能的正确性的几个重要的案例研究，如FIFO队列（短暂的和适用的实现）和左堆，从现有的OCaml库发出。
2021-09-06 cs.LO
Deductive Verification of Smart Contracts with Dafny
我们提出了一种开发经过验证的智能合约的方法。我们用验证友好的语言Dafny编写智能合约，它们的规范和实现。在我们的方法中，编写规范、实现和推理正确性的能力是主要关注的问题。我们提出了一个简单，简洁而强大的解决方案，推理合同，有外部调用。这包括任意重新进入，这是智能合约中错误和攻击的主要来源。虽然我们还没有一个从Dafny到EVM字节码的编译器，但我们在Dafny代码上获得的结果可以合理地假设在Solidity代码上也是如此：Dafny代码到Solidity的转换是简单的。因此，我们的方法可以很容易地用于开发和部署更安全的合同。
2022-08-04 cs.LO
Transaction Level Hierarchy Guided and Functional Coverage Driven Deductive Formal Verification
本文提出以事务级层次结构替代模块层次结构，通过增强 PDVL 并结合 Coq 的 DFV 流程，将功能覆盖率转化为证明义务，实现 100% 覆盖与证明复用。
2025-01-02 cs.AR cs.LO
A Framework for the Automated Verification of Algebraic Effects and Handlers (extended version)
代数效果和处理程序是构建非本地控制流机制的强大抽象，如可扩展异常、轻量级线程、协同例程、生成器和异步I/O。所有这些特征都具有非常进化的语义，因此它们对演绎验证技术提出了非常有趣的挑战。事实上，很少有人提出的技术来演绎验证具有这些结构的程序，甚至更少，当涉及到自动证明。在本文中，我们提出了一个扩展Cameleer，OCaml代码的演绎验证工具，允许一个原因的代数效果和处理程序。我们的建议使用异常嵌入效果和处理程序的行为，并采用去功能化来处理效果处理程序暴露的延续。
2023-02-07 cs.LO
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
Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL
该研究在Isabelle/HOL中机械化实现交互树，构建统一的模型执行与演绎验证框架，可支持多种程序与系统模型的验证及动画生成，保障执行与证明结果一致性。
2024-10-30 cs.LO
HaliVer: Deductive Verification and Scheduling Languages Join Forces
本文提出 HaliVer，将演绎验证器 Vercors 集成到 Halide 中，用同一规约验证算法及其调度生成的并行优化代码，显著减少标注并证明内存安全与功能正确性。
2024-01-19 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
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
Preguss: It Analyzes, It Specifies, It Verifies
针对LLMs在形式化验证中因上下文限制和复杂规范推断难导致的可扩展性问题，本文提出模块化细粒度框架Preguss，协同静态分析与演绎验证，通过RTE引导验证单元构建及LLM辅助单元级过程间规范合成，助力大规模程序自动化验证。
2025-08-20 cs.LO cs.SE
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
Verifying OpenJDK's LinkedList using KeY
作为一个特殊的情况下研究的形式化验证的国家的最先进的，真正的软件，我们讨论的规范和验证的正确版本的实现的链表所提供的Java集合框架。关键词：Java，标准库，演绎验证，KeY，Java建模语言，案例研究，错误
2019-11-11 cs.LO cs.SE
A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs
Zhejiang University（浙江大学）；Peking University（北京大学）；The Chinese University of Hong Kong（香港中文大学）；Xidian University（西安电子科技大学）；Beijing Institute of Control Engineering（北京控制工程研究所）
Preguss通过结合静态分析与演绎验证，实现大规模程序的自动化形式化验证，显著提升验证效率。
2026-03-10 cs.LO cs.SE
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
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
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
针对演绎验证中可满足含量词公式仅有无限模型、现有求解器只能找有限反例且易发散的问题，提出符号结构、符号模型搜索过程及涵盖多种类 EPR 的新可判定片段。
2024-09-10 cs.LO cs.PL
Forward Invariant Cuts to Simplify Proofs of Safety
使用演绎技术，如定理证明器，在混合系统的安全验证中有几个优点;然而，最先进的定理证明器需要大量的人工干预。此外，定理证明者在证明任务上取得进展所需的协助类型与系统设计者能够提供的阻力之间通常存在差距。本文提出了一种扩展的KeYmaera，演绎验证工具微分动态逻辑，新技术允许本地推理使用系统设计师的直觉，per-crossing在特定的模式作为证明任务的一部分。我们的方法允许定理证明者利用ward不变量，发现使用数值技术，作为安全性证明的一部分。我们引入了一个新的推理规则的证明演算的KeYmaera，前向不变切割规则，我们提出了一种方法来发现有用的前向不变，然后使用新的切割规则来完成验证任务。我们展示了我们的新方法可以用来完成验证任务，现有的演绎方法，我们的几个例子，包括一个涉及汽车动力系统控制系统的范围之外。
2015-08-10 cs.LO
Auto-active Verification of Graph Algorithms, Written in OCaml
函数式编程为构建结构正确的软件提供了完美的基础。这种范式的语言通常具有最先进的类型系统，良好的抽象机制和定义良好的执行模型。我们声称，所有这些都使得用函数式语言编写的软件成为正式认证的优秀目标。然而，令人惊讶的是，诸如演绎验证之类的技术很少应用于用主流函数式语言编写的大规模程序。在本文中，我们希望解决这种情况，并提出现实的OCaml实现的自动活动证明。我们选择从OCamlgraph库发布的实现作为我们的目标，因为这是一个大规模和广泛使用的OCaml代码。我们使用Cameleer，最近提出的OCaml程序的演绎验证工具，进行选定的案例研究的证明。绝大多数这样的证明都是使用SMT求解器全自动完成的，并且当需要时，我们可以在Why3 IDE中应用轻量级交互式证明（Cameleer将输入程序转换为等效的WhyML，Why3验证框架的语言）。据我们所知，这些是第一个用OCaml编写的图算法的机械化，大部分是自动化的证明。
2022-07-20 cs.LO
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
Predicate Transformer Semantics for Hybrid Systems: Verification Components for Isabelle/HOL
我们提出了一个语义框架的演绎验证的混合系统与Isabelle/HOL。它支持推理的时间演化的混合程序的差分动态逻辑建模的流或向量场的不变集的风格。我们介绍了这个框架的语义基础，并总结了他们的伊莎贝尔形式化以及由此产生的验证组件。一系列简单的例子展示了我们的工作方法。
2021-09-20 cs.LO
An Axiomatic Approach to Liveness for Differential Equations
提出了一种基于微分动态逻辑的常微分方程演绎活性验证方法。许多微妙之处使众所周知的离散活性验证技术（例如循环变体）到连续设置的推广复杂化。例如，ODE解可能在有限时间内爆炸，或者它们朝着目标的进展可能收敛到零。我们的方法通过使用ODE不变性属性（具有易于理解的演绎证明理论）连续细化ODE活性属性来处理这些微妙之处。这种方法是广泛适用的：我们在文献中调查了几个活性参数，并得出他们都是我们的公理化细化方法的特殊情况。我们还纠正了几个合理性错误的调查参数，这进一步突出了微妙的ODE活性推理和我们的演绎方法的效用。通过我们的方法确定的共同细化步骤库，使新的ODE活性证明规则的合理发展和理由，从我们的公理。
2019-07-10 cs.LO
The Structure of Differential Invariants and Differential Cut Elimination
混合系统验证的最大挑战是微分方程的处理。由于可计算的封闭形式的解决方案只存在于非常简单的微分方程，证明证书已经提出了更可扩展的验证。然而，这些证明证书的搜索过程仍然是相当特殊的，因为对问题结构的理解很差。我们研究微分不变量，它定义了微分方程的归纳原理，并且可以通过使用它们的微分结构来检查微分方程的不变性，而不必求解它们。研究了微分不变量的结构性质。为了分析证明搜索复杂性的权衡，我们确定了几类微分不变量之间的十几种关系，并比较了它们的演绎能力。作为我们的主要结果，我们分析了微分割的演绎能力和带有辅助微分变量的微分不变量的演绎能力。我们反驳了差分切割消除假设，并表明，与标准切割，差分切割的基本证明原则，严格增加了演绎能力。我们还证明了演绎能力进一步增加时，添加辅助微分变量的动态。
2012-11-23 cs.LO math.CA math.DS
An Update on Deductive Synthesis and Repair in the Leon Tool
我们报告我们的进展，在缩放演绎合成和修复的递归功能的Scala程序的莱昂工具。我们描述了新的技术，包括一个更精确的机制，用于编码有意义的候选程序的空间。我们的技术通过扩展我们可以合成的程序的空间和在许多情况下减少合成时间来增加合成的范围。作为一个新的例子，我们提出了一个行程长度编码函数的值列表，莱昂现在可以自动合成从规范组成的解码功能和本地最小值属性的编码值。
2016-11-23 cs.LO
Brownian Motion in Isabelle/HOL
为形式化验证机器人控制器中的随机混合系统，本文在Isabelle/HOL中机械化布朗运动、随机核与马尔可夫半群，并证明Kolmogorov-Chentsov定理以构造Hölder连续修正，为演绎验证奠定基础。
2024-10-13 cs.LO
Verification of the IBOS Browser Security Properties in Reachability Logic
本文给出了Illinois浏览器操作系统（IBOS）的重写逻辑规范，定义了可达性逻辑中的同源策略（SOP）等安全属性。它展示了如何使用我们的基于构造器的可达性逻辑定理证明器来演绎验证这些属性。本文还强调了证明中使用的推理技术和三个模块化原则，这些原则对扩大规模和完成验证工作至关重要。
2020-05-25 cs.CR cs.FL cs.LO
Automatic Program Instrumentation for Automatic Verification (Extended Technical Report)
本文提出将程序插桩作为统一验证范式，以自动变换方式消除规约语言中后端求解器难以处理的结构，并将数组聚合形式化为幺半群同态，在 MonoCera 工具中实现并验证其有效性。
2023-05-26 cs.LO cs.SE
Quantifying Software Correctness by Combining Architecture Modeling and Formal Program Analysis
本文提出 QuAC 模块化方法，结合面向服务架构建模、概率使用场景与演绎验证，用覆盖区域量化软件正确性，并基于 Palladio 与 KeY 的 Java 实现验证其可用性。
2024-01-25 cs.LO cs.SE
RustyDL: A Program Logic for Rust
Technische Universität Darmstadt（达姆施塔特工业大学）
RustyDL 是一种针对 Rust 的程序逻辑，旨在为自动交互式演绎验证工具提供基础，通过源代码级别推导提升复杂功能属性的验证能力。
2026-02-25 cs.LO cs.PL
Automatic Verification of Parametric Specifications with Complex Topologies
本文的重点是降低验证的复杂性，利用模块化在各个层次上：在规范，验证，和结构。对于规范，我们使用的模块化语言CSP-OZ-DC，它允许我们解耦验证任务有关的数据从那些有关的持续时间。在验证级别，我们利用模块化的定理证明丰富的数据结构，并使用此不变检查。在结构层面上，我们分析了模块化验证的系统组成的各种组件的相互作用的可能性，我们说明了这些想法，通过自动验证安全性能的案例研究，从欧洲训练控制系统标准，它扩展了以前的例子，包括一个复杂的轨道拓扑结构与列表的轨道段和列车与不同的路线。
2010-10-08 cs.LO cs.SE
BEval: A Plug-in to Extend Atelier B with Current Verification Technologies
本文介绍了BEval，Atelier B的扩展，以提高B方法或Event-B中验证活动的自动化程度。它结合了管理和验证软件项目的工具（Atelier B）和模型检查器/动画（ProB），以便用后者评估前者生成的验证条件。在我们的实验中，两个主要的验证策略（手动和自动）显示出显着的改善，ProB的评估证明补充工作室B内置的证明。我们使用微控制器指令集的B模型进行了实验;使用BEval自动验证了我们无法使用AtelierB的校准器自动或手动放电的几个验证条件。
2014-01-06 cs.LO cs.SE
Next Steps in LLM-Supported Java Verification
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）
本文初步展示如何利用演绎验证的严格工具集，从不可靠的LLM预言机中可靠地引导出正确的Java代码规约注解，为大规模软件系统提供可证明的正确性保证。
2025-02-03 cs.AI cs.LG cs.LO
Automatic verification and interactive theorem proving
自动验证是通过计算机验证正确性证书。相关的工具，通常称为证明助手或交互式证明器，提供了一个交互式环境，用于创建正式证书，其正确性可以完全自动地进行评估。这种系统在数学和计算机科学中都有应用，在数学中证书是定理的证明，在计算机科学中证书证明给定软件在其规范方面的正确性。
2017-01-13 cs.LO
Proceedings of the International Workshop on Verification of Scientific Software
本论文集收录了VSS 2025研讨会的成果，涵盖演绎验证、浮点误差分析等主题，旨在推动大规模科学代码的正确性与可靠性研究。
2025-10-14 cs.CE cs.LO
Partial Automation of Verification Condition Proving for Reflex Programs (Draft)
Novosibirsk State University（新西伯利亚国立大学）；Institute of Automation and Electrometry（自动化与电磁学研究所）
针对Reflex语言验证条件过多导致手动证明不可行的问题，提出通过引入注解语言、基于程序结构生成不变量以及使用SMT求解器来自动化部分验证条件的证明。
2026-06-23 cs.LO
A Program Instrumentation Framework for Automatic Verification
针对后端求解器难以处理部分规约语言结构的验证问题，提出统一的程序插桩验证范式，实现于MonoCera工具，可自动处理含数组量化、聚合操作的程序验证，并在含SV-COMP程序的样例上完成评估。
2024-12-09 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
Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version)
有界验证已被证明是有用的，以检测错误，并增加在程序的正确性的信心。与无界验证相比，通过（有界）内联进行调用和通过（有界）展开进行循环的推理不需要方法规范和循环不变式，因此将注释开销降低到最低限度，即要验证的属性的规范。对于基于传统程序逻辑的验证器，通过内联（和展开）来保存验证：成功的程序w.r.t.某些注释意味着内联程序的成功验证。也就是说，在内联程序中检测到的任何错误都揭示了原始程序中的真正错误。但是，这个基本属性可能不适用于自动分离逻辑验证器，如Caper、GRASShopper、RefinedC、Steel、VeriFast和基于Viper的验证器。在这种情况下，内联通常会更改方法执行所拥有的资源，这可能会影响自动证明搜索算法并引入虚假错误。在本文中，我们提出了第一种技术，验证保持内联自动分离逻辑验证。我们确定了一个语义条件的程序，并证明在Isabelle/HOL，它确保了验证保持内联的最先进的自动分离逻辑验证。我们还证明了一个双重结果：成功验证的内联程序，确保有方法和循环注释，使验证的原始程序有界执行。为了自动检查我们的语义条件，我们提出了两个近似，可以检查语法和程序验证器，分别。我们实现这些检查毒蛇，并证明他们是有效的非平凡的例子，从不同的验证。
2023-03-13 cs.LO
CISE3: Verificação de aplicações com consistência fraca em Why3
在这篇文章中，我们提出了一个工具，用于验证建立在顶级复制数据库上的程序。该工具评估顺序规范，并推断哪些操作需要同步，以便程序在分布式环境中正常运行。我们的原型是建立在演绎验证平台Why3。Why3框架提供了一个复杂的用户体验，扩展到现实案例研究的可能性，以及高度的自动化。一个案例研究和讨论，实验验证我们的方法的目的。
2019-09-09 cs.LO cs.PL
Compositional Verification for Timed Systems Based on Automatic Invariant Generation
我们提出了一种组合验证的方法，以解决状态空间爆炸问题固有的模型检查定时系统的大量组件。主要的挑战是获得相关的全球时间约束的组件单独的时间。为此，我们利用辅助时钟自动生成新的不变量，捕获组件之间的同步引起的约束。该方法已在RTD-STIM工具中实现，并在多个基准测试中成功实验。
2015-09-16 cs.LO
Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification
自动结构是由同步有限状态自动机表示的无限结构。本文关注有限词和树（排名/排名）的自动结构。我们调查的“有向版本”的拉姆齐量词，它表示存在一个无限的有向集团。这包含了拉姆齐量词的标准“无向版本”。首先观察到Ramsey量词与验证中的两个问题之间的有趣联系：（1）规则模型检验中Büchi和广义Büchi条件的可达性可以看作是传递自动图上的Ramsey量化（即，其边关系是传递的），（2）检查一元可分解性（a.k.a.可识别性）可以被看作是在共传递自动图上的Ramsey量化（即，其边关系是传递的补集）。我们提供了一个全面的复杂性景观拉姆齐量词在这三种情况下（一般，传递，共传递），所有NL和EXP之间。反过来，这产生了大量具有精确复杂性的新结果，例如，子树/扁平前缀重写的验证，以及树自动关系上的一元分解。我们还获得了相当简单的证明，例如，对于词自动关系上的一元可分解性的NL复杂度（由DFA给出）。
2023-02-13 cs.LO
A Practical Specification Language for Automatic Quantum Program Verification (Technical Report)
Institute of Information Science, Academia Sinica（中央研究院資訊科学研究所）；Graduate Institute of Electronics Engineering, National Taiwan University（国立台湾大学电子工程学研究所）；Faculty of Information Technology, Brno University of Technology（布尔诺理工大学信息技术学院）
本文提出了一种扩展的集合基规范语言和转换算法，通过控制自动机构造和量子位重排，实现线性复杂度的量子程序自动验证。
2026-05-07 cs.FL cs.LO
Toward Automatic Verification of Quantum Programs
本文总结了作者和他的合作者在量子程序的程序逻辑验证方法中所获得的结果，包括量子Hoare逻辑，量子程序的不变量生成和终止分析。为了更方便地对量子程序进行推理，还引入了证明大纲的概念和一些辅助规则。文章最后提出了今后研究的一些问题。
2018-07-31 cs.LO quant-ph
OSVAuto: automatic proofs about functional specifications in OS verification
本研究提出OSVAuto工具，通过编码OS常见数据类型命题为SMT形式并扩展序列量词实例化方法，实现uC-OS/II内核验证中大量函数规范证明义务的自动求解，降低证明工作量。
2025-05-22 cs.LO cs.SC
Automatic Verification of Correspondences for Security Protocols
我们提出了一种新的技术来验证安全协议中的对应关系。特别地，对应关系可以用于正式化认证。我们的技术是全自动的，它可以处理无限数量的会话的协议，它是有效的，在实践中。它大大扩展了以前的保密验证技术。该协议表示在一个扩展的π演算相当任意的密码原语。该协议表示包括要验证的对应关系的规范，但没有其他注释。这个表示然后被翻译成一个抽象的表示霍恩子句，这是用来证明所需的对应关系。我们的技术已被证明是正确的和实施。我们已经测试了它的各种协议从文献。实验结果表明，这些协议可以验证我们的技术在不到1 s。
2008-02-23 cs.CR cs.LO
Refinement Reflection: Complete Verification with SMT
我们介绍了精化反射，一个新的框架，用于建立基于SMT的演绎验证。关键思想是将实现用户定义函数的代码反映到函数的（输出）细化类型中。因此，在使用函数时，函数定义以允许可判定验证的精确方式在SMT逻辑中实例化。反射允许用户通过使用模式匹配和递归来编写其他程序来编写程序的等式证明，以执行大小写分解和归纳。因此，通过命题作为类型的原则，我们表明，反射允许规范的任意功能的正确性属性。最后，我们介绍了一个证明搜索算法，称为证明逻辑评估，使用技术从模型检验和抽象的解释，完全自动化的等式推理。我们已经在Liquid Haskell中实现了反射，并使用它来验证Monoid，Applicationative，Functor和Monad类型类的广泛使用的实例实际上满足使客户端安全所需的关键代数定律，并使用反射构建了第一个库，该库实际验证了关于关联性和排序的假设，这些假设对于安全的确定性并行性至关重要。
2017-11-09 cs.LO cs.PL
Formal Verification of Control Systems Properties with Theorem Proving
University of Bristol（布里斯托大学）
本文提出利用Why3工具对控制系统高阶属性进行演绎形式验证，包括稳定性、反馈增益和鲁棒性等。通过Simulink建模，提出三种主要步骤：指定模型信号属性、自动转换为Why3代码、自动验证属性。
2014-06-08 cs.LO cs.SY eess.SY
Verification of Provers and Solvers
University of Innsbruck（因斯布鲁克大学）
介绍自动推导工具与证明助手的连接方法，通过认证和验证等方式，回顾比较现有方法并提及成功应用。
2026-07-29 cs.LO cs.SC
Constraint-based automatic verification of abstract models of multithreaded programs
我们提出了一种多线程程序的抽象模型的自动验证技术，提供新鲜的名称生成，名称移动性和无界控制。作为高级规约语言，我们在这里采用了一个扩展的通信有限状态机的局部变量范围在一个无限的域名，称为TDL程序。通信机已被证明是非常有效的表示通信协议，以及表示多线程软件的抽象。我们提出的验证方法是基于编码的TDL程序成一个低级语言的基础上多集重写和约束，可以被看作是一个扩展的Petri网。通过这种编码，符号验证过程中开发的低级语言在我们以前的工作，现在可以应用到TDL程序。此外，编码使我们能够隔离TDL程序，仍然提供新鲜的名称生成，名称移动性和无界控制的可判定类的验证问题。我们的语法限制实际上是在线程的内部结构上定义的：为了获得一个完整的终止方法，线程最多只能有一个局部变量（范围在无限的域名上）。
2006-01-10 cs.LO cs.PL
Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution
在诸如分离逻辑之类的权限逻辑中，迭代分离合取是表示对堆位置的无界集合的访问权限的量词。与递归谓词相反，迭代分离合取并不规定它们所覆盖的位置的结构，因此不限制如何遍历和修改这些位置。这种灵活性对于验证随机存取数据结构（例如数组）和可以以多种方式遍历的数据结构（例如图形）是重要的。尽管它的有用性，没有自动程序验证原生支持迭代分离合取，他们是特别难以纳入符号执行引擎，流行的技术，为这些逻辑建立验证。在本文中，我们提出了第一个符号执行技术，以支持一般迭代分离合取。我们提出了一种新的表示符号堆和灵活的支持，量化堆位置的逻辑规范。我们的技术表现出可预测的和快速的性能，尽管在SMT级别采用量词，通过仔细控制量词实例。它与权限逻辑的其他功能兼容，如部分权限、递归谓词和抽象函数。我们的技术是实现作为一个扩展的毒蛇验证基础设施。
2016-05-06 cs.LO cs.PL
