Hyperproperty Verification as CHC Satisfiability
本文提出将∀ᵏ∃ˡ超属性验证问题归约为约束 Horn 子句可满足性问题，通过整合对齐与归纳不变式推断、结合博弈语义下的见证函数推断，实现超属性的可靠完备验证。
2024-01-31 cs.LO
Towards Proved Formal Specification and Verification of STL Operators as Synchronous Observers
本文提出将非嵌套离散时间 STL 公式编码为 Lustre 同步观察器，提供三值在线语义以支持性质验证与反例搜索，并通过仪表化证明确保实现正确性，实验使用 Kind2 和 Z3 自动化完成。
2023-11-16 cs.LO
Removing Unnecessary Variables from Horn Clause Verification Conditions
验证条件（Verification Conditions，VC）是一种逻辑公式，其可满足性保证了程序的正确性。我们认为VC的形式约束霍恩条款（CHC），这是自动生成的编码（解释器）的程序设计语言的操作语义。VC是通过基于展开/折叠变换规则的程序专门化而得到的，并且正如在专门化解释器时经常发生的那样，它们包含不必要的变量，即，在验证下的程序的正确性证明不需要的变量。在本文中，我们适应的CHC设置的一些技术，开发用于删除不必要的变量，从逻辑程序，我们表明，在某些情况下，这些技术的应用增加了霍恩子句求解器的有效性时，证明程序的正确性。
2016-07-15 cs.LO cs.PL cs.SE
Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types
我们报告的工作进展自动程序证明性能的程序写在高阶函数语言。我们的方法编码高阶程序直接作为一阶SMT问题的霍恩条款。将一阶程序的Hoare式验证简化为Horn子句的可满足性是很直接的。闭包的存在带来了一些挑战：相对完整的证明系统必须考虑闭包;在实践中，搜索过程的有效性取决于编码策略和底层求解器的能力。我们在这里使用代数数据类型来编码闭包，并依赖于支持代数数据类型的求解器。该方法的可行性进行检查使用的例子从文献中高阶程序验证。
2013-06-21 cs.LO
Sequential Convex Programming for the Efficient Verification of Parametric MDPs
最优性准则下参数马尔可夫决策过程的多目标验证问题可以自然地表示为非线性规划问题。我们观察到，许多这些计算要求的问题属于子类的符号程序。这种洞察力允许顺序优化算法有效地计算合理但可能次优的解决方案。该算法的每一步都解决了一个几何规划问题。这些几何规划是通过凸化原问题的非凸约束得到的。编码作为非线性程序的直接应用是模型修复和参数综合。我们证明了我们的方法的可扩展性和质量由著名的基准
2017-01-26 cs.LO
Operational semantics and program verification using many-sorted hybrid modal logic
Faculty of Mathematics and Computer Science, University of Bucharest（布加勒斯特大学数学与计算机科学学院）
本文提出基于多类型混合模态逻辑的框架，用于描述编程语言操作语义并验证程序正确性，相较于传统方法具有更自然的执行描述和更清晰的语义编码。
2025-11-27 cs.LO
Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic
Nagasaki University（长崎大学）；Toho University（东邦大学）
本文通过将皮亚诺算术中的Pi-0-1公式翻译为仅包含直觉主义指向谓词、0和后继函数的分离逻辑小片段，证明了标准模型下算术公式的有效性等价于该片段中翻译公式的有效性，并由此得出该片段不可判定的新证明。
2026-05-22 cs.LO
Formalizing the Soundness of the Encoding Methods of SAT-based Model Checking
有效的模型检验方法之一是利用SAT（或SMT）求解器的有效决策过程。在基于SAT的模型检验中，系统及其属性被编码成一组逻辑公式，并基于公式的可满足性来检验系统的安全性。随着编码方法的改进和制作（例如，k-induction和IC 3/PDR），验证它们的正确性变得更加重要。本研究旨在利用Coq证明助手对SMC方法进行形式化验证。我们的贡献是双重的：（1）我们将Coq中的基本编码方法、k-归纳法和IC 3/PDR（的简化版本）指定为一组简单的模块化编码谓词。(2)我们提供了一个正式的证明的合理性的编码方法的基础上，我们的形式化引理的状态序列和路径。
2022-03-11 cs.LO
Parameterized Verification of Algorithms for Oblivious Robots on a Ring
IRIF - Univ Paris Diderot（巴黎狄德罗大学 IRIF）；Sorbonne Universités, UPMC Univ Paris 06（索邦大学 皮埃尔和玛丽·居里大学）
我们研究验证问题的自主群的移动机器人，自组织和合作，以解决全球目标。特别是，我们专注于在本文中提出的模型由铃木和山下的匿名机器人在一个离散的空间与有限数量的位置（在这里，一个环）。已经提出了大量的算法工作的环，其大小不是先验固定的，因此可以被认为是一个参数。这些算法的手工正确性证明已被证明是容易出错的，最近的注意力已经给予了正式的方法来自动证明这些应用程序。我们的工作是第一个研究的验证问题，这样的算法在参数化的情况下。我们表明，安全性和可达性问题是不可判定的机器人异步进化。在积极的一面，我们表明，安全属性是决定在同步的情况下，以及在异步的情况下，一类特定的算法。协议的几个属性也可以决定。决策过程依赖于Presburger算法公式中的编码，该公式可以通过SMT求解器进行验证。我们的方法的可行性证明了几个案例研究的编码。
2017-06-16 cs.CC cs.DC cs.DS
Efficient Solving for Dynamic Data Structure Constraint Satisfaction Problem
Peking University（北京大学）；Primarius Technologies Co., Ltd.（普迈思科技有限公司）
本文提出动态数据结构约束满足问题(D2SCSP)的求解框架，通过依赖引导的问题划分和增量编码机制，提升求解效率，实验表明在工业基准上性能提升显著。
2026-04-04 cs.AR cs.FL cs.LO
Efficient CTL Verification via Horn Constraints Solving
时态逻辑的使用一直被认为是反应式系统的形式化规范和验证的基本方法。在本文中，我们采取的问题，自动验证的时间属性，由CTL公式，为一个给定的（可能是无限状态）的程序。我们提出了一种方法的基础上编码的问题作为一组霍恩约束。该方法以一个程序，建模为一个过渡系统，并作为输入的CTL公式给出的属性。首先利用CTL公式的句法结构生成一组普遍存在的量化Horn约束和良基约束。然后，通过应用现成的Horn约束求解引擎来求解生成的约束集。当且仅当生成的约束集有解时，程序才满足该性质。我们证明了实际的承诺的方法，通过将其应用于一组具有挑战性的例子。虽然我们的方法是基于一个通用的霍恩约束求解引擎，它是能够超越国家的最先进的方法专门为CTL验证。
2016-07-15 cs.LO
Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
本文为含循环、连续分布和条件化的概率程序验证奠定基础，通过黎曼和近似积分实现SMT不变量验证，并证明收敛性与完备性，且可在现有工具中应用。
2025-02-26 cs.LO cs.PL
Encodings of Bounded Synthesis
反应合成问题是计算满足时态逻辑中给定规范的系统。有界合成是我们接受的反应合成问题的解决方案的系统的最大尺寸的方法。其结果是，有界合成是可判定的，只要相应的验证问题是可判定的，并可以应用在经典的合成失败的设置，如在分布式系统的合成。本文研究有界综合背后的约束求解问题。我们考虑线性时间时序逻辑（LTL）的有界综合问题的约束系统作为布尔公式（SAT），量化的布尔公式（QBF），和依赖量化的布尔公式（DQBF）的不同减少。这些减少代表了简洁性和算法效率之间的不同权衡。在SAT编码中，系统的输入和状态都是显式表示的;在QBF中，输入是符号的，状态是显式的;在DQBF中，输入和状态都是符号的。我们使用反应合成竞赛（SYNTCOMP）和最先进的求解器的基准系统地评估编码。我们的关键，也许是令人惊讶的，实证发现是，QBF明显优于SAT和DQBF。
2018-03-26 cs.LO
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 New Interaction Concept for Interactive and Autoactive Program Verification
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）；Technical University of Darmstadt（达姆施塔特工业大学）
本文提出一种新的交互概念，允许用户在源代码和规范层面检查和交互证明状态，减少表示间的认知差距，并通过用户研究证明其对理解证明状态和发现代码或规范缺陷的益处。
2026-05-07 cs.LO cs.PL
Non-Deterministic Planning for Hyperproperty Verification
CISPA Helmholtz Center for Information Security（CISPA亥姆霍兹信息安全中心）
本文提出利用非确定性规划作为中间语言，将HyperLTL超属性验证问题转化为QDec-POMDP规划实例，并证明对HyperLTL大片段可归约为经典、FOND或POND规划，实验验证了方法的有效性。
2024-05-22 cs.AI cs.FL cs.LO
A verified algebraic representation of Cairo program execution
加密交互式证明系统提供了一种有效且可扩展的方法来验证区块链上的计算结果。一个证明器构造一个链外证明，证明程序在给定输入上的执行以某个结果终止。然后，证明者发布一个证书，该证书可以被有效地和可靠地验证，以普遍接受的密码学假设为模。该方法依赖于程序执行轨迹的代数编码。在这里，我们报告这样的编码的正确性的验证开罗模型的计算相对于STARK交互式证明系统，使用精益3证明助手。
2021-12-14 cs.CR cs.LO cs.PL
