(Quantified) Horn Constraint Solving for Program Verification and Synthesis
我们展示了如何自动工具的验证线性和分支的时间属性的程序，多线程，和功能的程序，以及程序合成可以自然地和统一地被视为求解器的约束条件的形式（量化）霍恩条款的背景逻辑理论。这样的观点可以提供各种优势，例如。例如，在一个实施例中，约束生成（也称为证明义务的生成）和约束求解（也称为证明发现）之间的关注点的逻辑分离、跨不同验证任务的求解器的重用、以及证明设计者从低级算法关注点中解放出来，反之亦然。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
2014-05-29 cs.LO
Interpolant Tree Automata and their Application in Horn Clause Verification
本文研究了凸多面体域上的抽象解释与插值树自动机相结合的Horn子句验证的抽象-精化方案。这些技术以前已经单独应用，但在本文中以一种新的方式相结合。内插树自动机的作用是在精化过程中提供一个伪反例的概括，捕获一组可能无限的伪反例迹。在我们的方法中，这些痕迹，然后消除使用的Horn子句的变换。我们比较这种方法与其他两种方法，其中之一使用插值树自动机的算法跟踪抽象和细化，而另一个使用抽象的解释没有概括步骤的凸多面体的域。一些霍恩子句验证问题的实验结果的评价表明，插值树自动机与抽象解释的组合给出了一些增加的验证工具的力量，而有时会产生的性能开销。
2016-07-10 cs.LO
Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification
我们提出了一种方法来约束霍恩子句（CHC）验证相结合的三种技术：抽象的解释在一个域的凸多面体，专门化的约束条件在CHC使用抽象解释的查询答案转换的条款，和细化分裂谓词。的工作的目的是调查如何分析和转换工具开发的约束逻辑程序（CLP）可以适用于霍恩子句验证问题。凸多面体的抽象解释能够推导出复杂的不变量，当与传播约束的专业化结合使用时，它可以经常解决具有挑战性的验证问题。这本身就是一个贡献，但是当它失败时需要精化，并且如何精化凸多面体分析的问题还没有被研究很多。我们提出了一种改进技术的基础上插值来自一个反例跟踪，这些都是用来驱动基于属性的专业化，分裂谓词，进而导致更精确的凸多面体分析。专业化，分析和分裂的过程可以重复，以类似于CEGAR和迭代专业化方法的方式。
2014-12-03 cs.LO
Submodel Enumeration for CTL Is Hard
该研究针对CTL模型枚举任务，证明无论使用CTL算子的哪个子集，枚举满足公式的子模型都具有计算难度，同时提出了基于布尔函数限制、可快速枚举的CTL片段。
2023-12-15 cs.CC cs.LO
On Sufficient and Necessary Conditions in Bounded CTL: A Forgetting Approach
Guizhou University（贵州大学）；Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）；National University of Defense Technology（国防科技大学）
计算树逻辑（CTL）是形式化验证的核心形式之一。作为一种规约语言，它被用来表达一个系统期望满足的属性。从验证和系统设计的角度来看，由于各种原因，这种属性的某些信息内容可能变得与系统无关，例如，时间久了，可能会过时，又或因实际困难而不可行。然后，问题出现在如何减去这样的信息，而不改变相关的系统行为或违反现有的规范在一个给定的签名。此外，在这种情况下，两个关键概念是信息：给定属性的最强必要条件（SNC）和最弱充分条件（WSC）。为了解决这样的情况下，在一个原则性的方式，我们介绍了一个基于遗忘的方法在CTL和显示，它可以用来计算SNC和WSC的属性下，一个给定的模型和一个给定的签名。我们研究了它的理论性质，也表明我们的概念满足现有的知识遗忘的基本假设。此外，我们分析了一些基本的推理任务的计算复杂性的碎片CTL_AF。
2020-07-03 cs.AI cs.LO
Abstract Family-based Model Checking using Modal Featured Transition Systems: Preservation of CTL* (Extended Version)
变量系统允许通过使用特征（配置选项）标记变量功能来有效地构建许多自定义变量。在许多应用中，其质量保证和形式化验证至关重要。基于族的模型检验通过利用变量之间的共性，允许在单次运行中同时验证变分系统的所有变量。然而，它的计算成本仍然在很大程度上取决于变体的数量（通常是巨大的）。在这项工作中，我们将展示如何实现有效的基于家庭的模型检验的CTL* 的时间属性，使用可变性抽象和现成的（单系统）工具。我们使用变异抽象派生抽象的基于族的模型检验，其中的变异模型的变分系统被替换为一个抽象的（更小的）版本，称为模态特征的过渡系统，它保留了普遍的和存在的时间属性的满意度，在CTL* 表示。模态特征变迁系统包含两类变迁，分别称为may变迁和must变迁，它们分别由保守（过近似）抽象和它们的对偶（欠近似）抽象定义。可变性抽象可以与变量集合的不同划分相结合，以推断用于变分系统的合适的分而治之验证计划。我们说明了几个变分系统的这种方法的实用性。
2018-03-05 cs.LO cs.PL cs.SE
Decomposition by tree dimension in Horn clause verification
在本文中，我们调查使用的概念树维Horn子句的分析和验证。树的维数是其非线性的度量-例如，任何长度的列表的维数为零，而完全二叉树的维数等于其高度。我们将这个概念应用到对应于Horn子句推导的树。一个给定的Horn子句集P可以转化为一个新的子句集P=<k，其派生树是P的派生树的子集，其维数不超过k。类似地，可以从其导出树具有至少k + 1的维度的P获得子句集合P>k。为了证明P的所有导子的一些性质，我们系统地应用这些变换，对于不同的k值，将证明分解为P= k的单独证明<k and P>（可以并行执行）。我们展示了一些初步的结果表明，分解树维是一个潜在的有用的证明技术。我们还研究了使用现有的自动证明工具来证明给定程序的可行导出树的维数的一些有趣的性质。
2015-12-12 cs.LO
Tree dimension in verification of constrained Horn clauses
在本文中，我们将展示如何使用树维的概念，在验证的约束Horn子句（CHCs）。树的维数是其分支复杂性的数值度量，这里的概念适用于Horn子句派生树。零维的导出树对应于使用线性CHC的导出，而更高维的树来自使用非线性CHC的导出。我们展示了如何仪器CHC谓词与一个额外的参数的尺寸，允许CHC验证器的原因对衍生物的尺寸上的界限。给定一个CHCs集合$P$，我们定义了$P$的一个变换，产生一个维度有界的CHCs集合$P^{\leq{k}}$。$P^{\leq{k}}$的推导集合由维数最多为$k$的$P$的推导组成。我们还展示了如何构造一组表示为$P^{>{k}}$的子句，其派生具有超过$k$的维度。然后，我们提出了使用这些结构分解CHC验证问题的算法。这种分解的一个变化考虑连续增加维度的导数。本文包括实施和实验结果的描述。《逻辑程序设计理论与实践》（Theory and Practice of Logic Programming，TPLP）
2018-03-06 cs.LO
Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis
本卷包含第八届Horn Clauses for Verification and Synthesis研讨会（HCVS）的后续会议记录，该研讨会实际上是由于Covid-19大流行而作为ETAPS的附属研讨会而举行的。
2021-09-09 cs.LO cs.SE
Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis
本卷包含HCVS 2016的会议记录，第三届Horn Clauses for Verification and Synthesis研讨会于2016年4月3日在荷兰埃因霍温举行，作为欧洲软件理论与实践联合会议（ETAPS 2016）的卫星活动。许多感兴趣的程序验证和综合问题可以直接使用Horn子句建模，CLP和CAV社区的许多最新进展都集中在有效地解决Horn子句提出的问题上。第三次Horn子句验证和综合研讨会的举办旨在汇集约束/逻辑编程和程序验证两个社区的研究人员，讨论基于Horn子句的分析，验证和综合。这两个群体在不同的时间从不同的角度倡导关于核查和综合的霍恩条款，举办这次讲习班是为了促进互动和富有成效的经验交流和融合。
2016-07-14 cs.LO cs.PL
Generalised Interpolation by Solving Recursion-Free Horn Clauses
在本文中，我们提出了InterHorn，无递归Horn子句的求解器。InterHorn的主要应用领域在于解决软件验证中出现的插值问题。我们展示了如何一系列的插值问题，包括路径，过渡，嵌套，状态/过渡和良好的插值可以直接由InterHorn处理。通过详细说明这些插值问题和他们的霍恩子句表示，我们希望鼓励出现一个共同的后端插值接口有用的不同的验证工具。
2014-12-03 cs.LO
The Relationship between Craig Interpolation and Recursion-Free Horn Clauses
尽管经过数十年的研究，软件程序中仍然有许多常见的概念被认为对验证具有挑战性：其中包括并发性以及程序与过程的组合分析。作为一个有前途的方向，以克服这些困难，最近使用的Horn约束作为软件程序的中间表示已被提出。Horn约束与Craig插值有关，Craig插值是用于在验证中构造和细化抽象以及合成归纳循环不变量的主要技术之一。我们给出了一个调查的不同形式的克雷格插值在文献中发现，并表明，它们都对应于自然片段（递归自由）霍恩约束。我们还讨论了解决递归自由霍恩约束系统的技术。
2013-02-18 cs.LO
Proceedings First Workshop on Horn Clauses for Verification and Synthesis
本卷包含HCVS 2014的会议记录，第一次Horn Clauses for Verification and Synthesis研讨会于2014年7月17日在奥地利维也纳举行，作为联邦逻辑会议（FLoC）的卫星活动和维也纳逻辑夏季（VSL 2014）的一部分。HCVS 2014隶属于第26届计算机辅助验证国际会议（CAV 2014）和第30届逻辑编程国际会议（ICLP 2014）。大多数感兴趣的程序验证和综合问题可以直接使用Horn子句建模，并且约束/逻辑编程和程序验证社区的许多最新进展都集中在有效地解决Horn子句提出的问题上。由于这些团体在不同的时期从不同的角度倡导关于核查和综合的Horn条款，因此举办HCVS研讨会是为了促进互动和富有成效的经验交流和整合。
2014-12-02 cs.LO cs.SE
Proceedings 5th Workshop on Horn Clauses for Verification and Synthesis
许多感兴趣的程序验证和综合问题可以直接使用Horn子句建模，CLP和CAV社区的许多最新进展都集中在有效地解决Horn子句提出的问题上。HCVS系列研讨会旨在汇集在约束/逻辑编程两个社区工作的研究人员（例如，ICLP和CP），程序验证（例如，CAV、TACAS和VMCAI）和自动演绎（例如，CADE，IJCAR），关于基于Horn子句的分析、验证和综合的主题。这些团体在不同的时期从不同的角度倡导关于核查和综合的霍恩条款，组织HCVS是为了促进互动和富有成效的经验交流和整合。
2018-09-12 cs.LO cs.PL cs.SE
Proceedings of the 12th Workshop on Horn Clauses for Verification and Synthesis
本论文集收录2025年7月在克罗地亚萨格勒布举办的、作为CAV 2025附属会议的第12届HCVS研讨会的会后论文。
2025-10-29 cs.LO cs.PL cs.SE
A Theory of Heap for Constrained Horn Clauses (Extended Technical Report)
约束Horn子句（CHC）是一种中间程序表示，可以由几个验证工具生成，并且可以由许多Horn求解器处理和求解。在验证中使用CHC时的主要挑战之一是堆分配的数据结构的编码：这种数据结构今天要么使用数组理论显式表示，要么在不变量或细化类型的帮助下转换，击败CHC作为语言独立的表示以及Horn求解器实现的算法的不可知性。本文提出了一种适用于CHC的SMT-LIB堆理论，目的是为具有堆数据结构的程序提供一种标准的交换格式。我们介绍了堆理论的语法，定义其语义的公理和使用减少SMT-LIB数组和数据类型，并讨论其属性和大纲可能的扩展和未来的工作。
2021-04-09 cs.LO
Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types
我们报告的工作进展自动程序证明性能的程序写在高阶函数语言。我们的方法编码高阶程序直接作为一阶SMT问题的霍恩条款。将一阶程序的Hoare式验证简化为Horn子句的可满足性是很直接的。闭包的存在带来了一些挑战：相对完整的证明系统必须考虑闭包;在实践中，搜索过程的有效性取决于编码策略和底层求解器的能力。我们在这里使用代数数据类型来编码闭包，并依赖于支持代数数据类型的求解器。该方法的可行性进行检查使用的例子从文献中高阶程序验证。
2013-06-21 cs.LO
Analysis and Transformation of Constrained Horn Clauses for Program Verification
本文综述了最近的工作应用分析和转换技术，起源于约束逻辑编程（CLP）领域的问题，验证软件系统。我们提出了基于专业化的技术翻译验证问题，为不同的程序设计语言，并在一般的软件系统，到满足性问题的约束霍恩条款（CHCs），一个术语，已成为流行的验证领域，指CLP程序。然后，我们描述了静态分析技术的CHCs，可用于推断相关的程序属性，如循环不变。我们还概述了一些转换技术的基础上专业化和折叠/展开规则，这是有用的，以提高CHC可满足性工具的有效性。最后，我们讨论了应用这些技术的未来发展。
2021-08-02 cs.LO cs.PL
An encoding of array verification problems into array-free Horn clauses
自动验证程序的安全属性是困难的，如果程序作用于数组或其他形式的映射，则更难。存在许多方法来验证程序操作上的布尔和整数值（例如抽象的解释，反例引导的抽象细化使用插值），但转置它们数组属性已充满了困难。与大多数以前的方法相比，我们不引入一个新的抽象域或一个新的插值过程数组。相反，我们生成一个抽象的标量问题，并将其提供给一个预先存在的求解器，与可调precision.Our转换的问题表示使用霍恩条款，一个共同的格式与明确和明确的逻辑语义验证问题。我们的编码的一个重要特点是，它创建了一个非线性的霍恩问题，与树展开，即使下面的“平坦”的控制图结构通常会产生一个线性的霍恩问题，与线性展开。也就是说，我们的编码不能表示成另一个控制流图问题的编码，并真正利用霍恩子句格式的能力。我们说明了我们的方法与选择排序的功能正确性的完全自动化的证明。
2015-09-30 cs.LO cs.PL
A Fixed-point Theorem for Horn Formula Equations
我们考虑约束霍恩条款解决从更一般的角度来看，解决公式方程。约束Horn子句对应于Horn公式方程的子类。本文提出并证明了Horn公式方程的一个不动点定理，该定理基于将Horn子句集的极小模型在对象层次上的不动点计算表示为一阶逻辑中的公式，并给出了一个最小不动点算子.我们描述了这个不动点定理的几个推论，特别是关于程序验证的逻辑基础，并勾勒出如何概括它，将抽象的解释。
2021-09-10 cs.LO
Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis
会议记录包括阿尔贝托的主题论文，随后由洛伦佐克莱门特（美国）撰写的6份邀请论文。华沙），阿兰芬克尔（美国。Paris-Saclay），John Gallagher（Roskilde U.和IMDEA软件研究所）等，尼尔·琼斯（美国）Copenhagen）等人，Michael Leuschel（Heinrich-Heine U.）和Maurizio Proietti（IASI-CNR）等人。这些邀请论文之后是VPT 2020上接受的4篇常规论文和HCVS 2020的论文，其中包括三篇投稿论文和一篇关于第三届约束Horn子句求解器竞赛的邀请论文。此外，Andrzej Skowron（U.华沙），索菲雷诺（EPO）和莫阿约翰逊（查尔默斯大学），包括在内。
2020-08-06 cs.LO cs.PL cs.SC
Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation
这些会议记录包括在第九届验证和合成霍恩条款研讨会和第十届验证和程序转换国际研讨会上提交的选定论文，这两个研讨会都隶属于ETAPS 2022。许多感兴趣的程序验证和综合问题可以直接使用Horn子句建模，CLP和CAV社区的许多最新进展都集中在有效地解决Horn子句提出的问题上。HCVS系列研讨会旨在汇集在约束/逻辑编程社区工作的研究人员（例如，ICLP和CP），程序验证（例如，CAV、TACAS和VMCAI）和自动演绎（例如，CADE，IJCAR），关于基于Horn子句的分析、验证和综合的主题。这些团体在不同的时期从不同的角度倡导关于核查和综合的霍恩条款，组织HCVS是为了促进互动和富有成效的经验交流和整合。VPT研讨会的目的是汇集在程序验证和程序转换领域工作的研究人员。这两个领域之间有很大的潜力进行有益的互动，因为：1）一方面，在程序转换领域开发的方法和工具，如部分评估，折叠/展开转换和超级编译，都已成功应用于验证无限状态和参数化系统。2)另一方面，模型检验，抽象解释，SAT和SMT解决和自动定理证明已被用来加强程序转换技术。此外，程序转换工具的正式认证，如自动重构工具和编译器，最近吸引了相当大的兴趣，提出了重大挑战。
2022-11-19 cs.LO cs.PL cs.SC
Removing Unnecessary Variables from Horn Clause Verification Conditions
验证条件（Verification Conditions，VC）是一种逻辑公式，其可满足性保证了程序的正确性。我们认为VC的形式约束霍恩条款（CHC），这是自动生成的编码（解释器）的程序设计语言的操作语义。VC是通过基于展开/折叠变换规则的程序专门化而得到的，并且正如在专门化解释器时经常发生的那样，它们包含不必要的变量，即，在验证下的程序的正确性证明不需要的变量。在本文中，我们适应的CHC设置的一些技术，开发用于删除不必要的变量，从逻辑程序，我们表明，在某些情况下，这些技术的应用增加了霍恩子句求解器的有效性时，证明程序的正确性。
2016-07-15 cs.LO cs.PL cs.SE
Verification of Time-Aware Business Processes using Constrained Horn Clauses
我们提出了一种方法来验证时间感知的业务流程，即业务流程中的活动的时间约束是明确考虑的属性。业务流程是使用业务流程建模表示法（BPMN）的扩展来指定的，持续时间是通过整数约束来定义的。操作语义的定义由一组受约束的Horn子句（CHC）OpSem给出。我们的验证方法包括两个步骤。(Step 1）我们专门针对一个给定的业务流程和一个给定的时间属性进行验证，从而得到一组CHC，其可满足性相当于给定属性的有效性。(Step 2）我们使用最先进的CHC求解器来检查这些子句集的可满足性。我们已经实现了我们的验证方法，使用VeriMAP转换系统，和Eldarica和Z3求解器的CHCs。
2016-08-09 cs.LO cs.SE
Verification of Programs by Combining Iterated Specialization with Interpolation
我们提出了一个程序安全的验证技术，结合迭代专业化和插值霍恩子句求解。我们的新方法组合在一起，这两种技术在一个模块化的方式，利用共同的霍恩子句表示的验证问题。迭代专业化验证器通过使用展开/折叠等价保持转换规则来转换验证条件的初始集合。在转换过程中，程序不变量是通过应用加宽运算符来发现的。然后通过插值霍恩子句求解器分析专用验证条件的输出集，从而将插值的效果添加到加宽的效果中。特殊化和插值阶段可以迭代，也可以与其他改变约束传播方向的转换（从程序前提条件向前或从错误条件向后）相结合。我们已经实现了我们的验证技术集成VeriMAP验证器与FTCLP霍恩条款求解器，迭代专业化和插值的基础上，分别。我们的实验结果表明，集成验证器提高了每个单独运行的组件的精度。
2014-12-03 cs.LO cs.SE
HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)
HornStr 是首个将正则模型检验的不变式合成转化为字符串上的约束 Horn 子句问题的求解器，支持 L* 和基于 SAT 的自动机学习，并自动验证 MU 谜题，生成超 30000 个新基准。
2025-05-23 cs.FL cs.LO
Interval-based Resource Usage Verification by Translation into Horn Clauses and an Application to Energy Consumption
许多应用程序需要符合规范，约束资源的使用，如执行时间，能源，带宽等，我们已经提出了一个可配置的框架，静态资源使用验证规范可以包括下限和上限，数据大小相关的资源使用功能。为了静态地检查这些规范，我们的框架推断出相同类型的资源使用函数，这些函数安全地近似于程序的实际资源使用，并将它们与规范进行比较。我们回顾这个框架如何支持几种语言和编译输出格式，通过将它们翻译成基于Horn子句的中间表示，并使用该框架的可配置性来描述输入语言的资源语义。我们提供了一个更详细的形式化和扩展的框架，使资源使用规范和分析/验证输出可以包括前提条件表达区间的输入数据大小的断言是适用的，证明，或反驳。最重要的是，我们还扩展了可以检查的函数类。我们提供的Ciao/CiaoPP框架内的实施结果，并报告通过实例化这个框架的能源消耗规范的验证命令/嵌入式程序的工具。这篇论文正在考虑发表在《逻辑程序设计理论与实践》（TPLP）上。
2018-03-12 cs.LO cs.PL
Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification
提出针对线性约束Horn子句的自底向上验证方法，在THETA框架中相比自顶向下技术使解决任务数量增加两倍多。
2024-04-23 cs.LO cs.SE
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
我们提出了一个组合SMT为基础的算法的安全程序，考虑到堆以及。现有的基于SMT的方法要么在很大程度上限于处理线性算术运算和属性，或者是非组合的。我们使用约束角子句（CHCs）来表示验证条件，其中使用阵列的扩展理论（ARR）的内存操作建模。首先，我们描述了一个指数时间量词消去（QE）算法的ARR，它可以引入新的量词的索引和值排序。其次，我们适应QE算法，以有效地获得下近似使用模型，从而在多项式时间基于模型的投影（MBP）算法。第三，我们集成的MBP算法的框架中的组合推理的过程性程序使用的可能和必须的摘要，我们最近提出的。我们对CHC的解决方案目前仅限于无量词公式。最后，我们描述了我们的实践经验，在SV-COMP'15基准测试中使用的工具SPACER的实现。
2015-08-06 cs.LO cs.PL cs.SE
Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis
本卷为LSFA 2023与HCVS 2023的会后论文集，涵盖逻辑与语义框架、Horn子句验证与综合等主题。
2024-04-21 cs.LO cs.PL cs.SC
CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses
本文提出基于组合策略的CHC求解器CHCVERIF，复用成熟软件验证工具求解CHC问题，验证了该思路的可行性与潜力。
2025-10-30 cs.LO cs.PL cs.SE
Symbolic Model Checking using Intervals of Vectors
Computer Science Department Faculty of Science University of Geneva（日内瓦大学理学院计算机科学系）
本文提出了一种基于向量区间的新方法，用于高效进行Petri网的CTL模型检查，通过同态操作和标准形式提升性能。
2026-09-16 cs.LO
Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification
程序性质的证明可以归结为一组约束Horn子句（CHC）的可满足性证明，这些约束Horn子句可以由程序和程序性质自动生成。在本文中，我们已经进行了一个案例研究，在霍恩子句验证，考虑几个排序程序的转换技术，使我们能够消除归纳数据结构，如列表或树的有效性进行了探索。如果这种技术是成功的，我们得到一组CHC的整数和布尔值的约束，可满足性检查通常可以通过使用最先进的CHC求解器，如Eldarica或Z3，以有效的方式进行。在这个案例研究中，我们还说明了一个配套技术的有用性的基础上引入所谓的差异谓词，其定义对应于在验证过程中所需的引理。我们已经考虑了实现以下类型的排序算法作用于整数列表的函数程序：（i）线性递归排序算法，如插入排序和选择排序，以及（ii）非线性递归排序算法，如快速排序和合并排序，我们已经考虑了以下性质：（i）部分正确性属性，即输出列表的有序性，以及当被视为多集时输入和输出列表的相等性，以及（ii）一些算术属性，例如排序之前和之后的元素之和相等。
2019-07-09 cs.LO cs.PL cs.SC
ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses
本文提出加速驱动子句学习（ADCL）演算，利用循环加速避免递归 CHCs 在归结证明中的重复推导，从而缩短证明，并在 LoAT 中实现后与现有工具实证比较。
2023-07-14 cs.LO
Higher-Order Constrained Horn Clauses and Refinement Types
出于高阶函数程序自动验证中的应用，我们开发了一个概念的约束霍恩条款在高阶逻辑和决策问题，其可满足性。我们表明，虽然高阶子句的可满足系统一般不具有最小模型，有一个规范模型的概念，通过减少到一种单调逻辑程序的问题。在高阶程序验证的工作之后，我们开发了一个细化类型的系统，以推理和自动搜索模型。这为解决决策问题提供了一个合理但不完整的方法。最后，我们证明了一个扩展的决策问题，其中细化类型直接用作警卫存在量词可以减少到原来的问题。这个结果可以用来表明，高阶函数的性质，可定义使用细化类型也表示使用高阶约束霍恩子句。
2017-08-01 cs.LO cs.PL
Solving non-linear Horn clauses using a linear solver
开发有效的非线性Horn子句求解器是一项具有挑战性的任务，因为求解器必须推理树结构而不是线性求解器中的线性结构。在本文中，我们提出了一个增量的方法来解决一组非线性霍恩条款使用线性霍恩条款求解器。我们通过交错的程序变换和线性求解器来实现这一点。程序转换是基于树维的概念，我们将其应用到对应于Horn子句派生的树。树的维数是衡量其非线性的一个指标，例如一个线性树（其节点最多有一个子节点）的维数为零，而一个完整的二叉树的维数等于其高度。给定的Horn子句集合$P$可以被转换成新的子句集合$P^k$（其导出树是$P$的导出树的子集，其维度至多为$k$）。我们首先用$k=0$生成$P^k$，它根据定义是线性的，然后将其传递给线性求解器。如果$P^k$有解$M$，并且是$P$的解，则$P$有解$M$。如果$M$不是$P$的解，我们将$M$插入到$P^{(k+1)}$，它再次变为线性，并将其传递给求解器，并继续连续增加$k$的值，直到我们找到$P$的解或资源耗尽。在一些Horn子句验证基准上的实验表明，这是一种使用线性求解器求解非线性Horn子句集的有前途的方法。这表明，对于$P$的某些欠近似$P^k$，得到的解在很多情况下变成了$k$的相当小的值的$P$的解。
2015-11-20 cs.LO
Contract Strengthening through Constrained Horn Clause Verification
一个程序的函数属性通常通过为它的每个函数提供一个契约来指定。一个函数的契约由一对公式组成，称为前置条件和后置条件，它们分别在该函数执行之前和之后保持有效。可能的情况是，程序员提供的契约不足以允许验证系统证明程序的正确性，也就是说，对于每个函数，如果前置条件成立，并且函数的执行终止，则后置条件成立。我们解决这个问题，通过提供一种技术，可以加强后置条件的功能，从而提高验证程序的正确性的能力。我们的技术包括四个步骤。首先，翻译的给定程序，它可以操纵代数数据结构（ADT），其合同成一组受约束的霍恩条款（CHC）的可满足性意味着给定的合同的有效性。然后，通过由VeriCaT工具执行的CHC转换，导出一组新的CHC，这些CHC仅操作基本排序（例如布尔或整数），并且其可满足性暗示了原始子句集的可满足性。然后，使用CHC求解器SPACER为基本排序构造新的派生CHC的模型（如果有的话）。最后，将该模型转化为适当加强给定合同的后置条件的公式。我们将通过一个由Scala程序组成的用于反转列表的示例来展示我们的技术。请注意，当考虑给定的合同时，Stainless验证器无法证明该程序的正确性，而当考虑通过应用我们的技术构造的具有增强后条件的合同时，它成功了。
2022-11-22 cs.LO cs.PL
A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
在以前的论文中，我们已经表明，条款集属于霍恩Bernays-Schönfinkel片段在简单的线性实算术（HBS（SLR））可以转换为HBS条款集在一个有限的一阶常数。翻译保持有效性和可满足性，如果我们用正的普遍或存在性量化验证条件（条件）扩展我们的输入，它仍然适用。我们称这种翻译为数据锤。它的SPASS-SPL实现与数据库推理器VLog相结合，建立了一个有效的方式来决定验证条件的霍恩片段。我们验证了两个例子：一个车道变换助理的汽车和增压内燃机的电子控制单元的监督代码。在本文中，我们改进我们的Datasheet锤子在几个方面：我们将其推广到混合实整数算术和有限的一阶排序;我们扩展了可接受的不平等超出变量界限和正接地不等式的类;我们显着降低了锤子输出的大小由软类型的纪律。我们称之为排序后的数据锤。它不仅允许我们处理更复杂的管理程序代码，并更简洁地建模已经考虑过的管理程序代码，而且还提高了我们在真实世界基准测试示例中的性能。最后，我们取代之前的SPASS-SPL和VLog之间的基于文件的接口的紧密耦合，导致一个单一的可执行的二进制文件。
2022-01-24 cs.LO
An abstract fixed-point theorem for Horn formula equations
TU Wien（维也纳工业大学）；University of Amsterdam（阿姆斯特丹大学）
针对计算机科学多应用中重要的Horn公式方程，本文在带最小不动点算子的一阶逻辑中证明了适用于抽象语义的抽象不动点定理，并阐述其在程序验证逻辑基础等计算逻辑领域的推论。
2025-11-11 cs.LO math.LO
An iterative approach to precondition inference using constrained Horn clauses
我们提出了一种方法，用于自动推理的条件上的初始状态的程序，保证在程序中的安全断言不被违反。约束霍恩条款（CHCs）被用来建模的程序和断言在一个统一的方式，我们使用标准的抽象解释，得出一个过度近似的不安全的初始状态。前提条件则是对应于该集合的补集的约束，欠近似安全初始状态的集合。这种互补的想法并不新鲜，但以前试图利用它的尝试已经失去了精确性。在这里，我们开发了一种迭代专门化算法，以提供更精确的，在某些情况下最佳的安全条件。该算法结合了现有的转换，即约束专业化，部分评估和消除痕迹的转换。这些转换中的最后两个执行多变量专门化，从而导致提高精度的析取约束。该算法的实现和测试的基准套件的程序从文献中的前提推理和软件验证比赛。
2018-04-17 cs.LO
Solving non-linear Horn clauses using a linear Horn clause solver
在本文中，我们表明，检查可满足性的一组非线性霍恩条款（也称为非线性霍恩条款计划）可以实现使用求解器的线性霍恩条款。我们实现这一点，通过交错的程序转换与线性霍恩条款（也称为线性霍恩条款求解器）的可满足性检查。程序转换是基于树维度的概念，我们将其应用于一组非线性子句，产生一组其派生树具有有界维度的集合。这样一套条款可以线性化。然后，主要的算法进行应用线性化变换和求解器的线性霍恩条款的一系列条款的连续增加的维度范围。然后，通过使用较低维度的条款解决方案来（部分）线性化较高维度的条款，进一步发展了该方法。我们构建了一个原型实现这种方法，并进行了一些实验上的一组验证问题，这表明了一些承诺。
2016-07-15 cs.LO cs.PL
Theta as a Horn Solver
本文针对验证框架Theta在CHC领域技术细节未明的问题，详述其算法特性与基于CHC-COMP基准的优缺点，修正2025届竞赛配置问题后重测并报告其真实性能。
2025-10-30 cs.LO cs.SE
Constraint-based Relational Verification
近年来，他们已经有许多作品，旨在自动化关系验证。同时，尽管约束Horn子句（CHC）赋予了广泛的验证技术和工具，但它们缺乏表达$k$之外的超属性的能力-安全性，如广义非干扰和共同终止。本文介绍了一种新的和全自动的基于约束的关系验证方法。我们首先介绍了一类新的谓词约束满足问题称为pfwCSP的约束表示为子句模一阶理论的谓词变量的三种：普通的，良好的基础，或功能。这种对CHC的推广允许任意的（即，可能非Horn）子句、良好基础约束、功能约束，并且能够表达这些关系验证问题。我们的方法使我们能够表达和自动验证需要非平凡的问题实例（即，非顺序和非锁步）自合成，这是通过自动推断适当的指示何时以及哪个程序副本移动的指示符（或对齐）来实现的。为了解决这个新的语言中的问题，我们提出了一个约束求解方法pfwCSP的基础上分层反例引导归纳合成（CEGIS）的普通，良好的基础，和功能谓词。我们已经实现了所提出的框架，并取得了可喜的成果，在不同的关系验证问题，超出了以前的验证框架的范围。
2021-06-04 cs.LO cs.PL
Verification of Logical Consistency in Robotic Reasoning
University of Sheffield（谢菲尔德大学）
大多数自主机器人代理使用逻辑推理来保持自己的安全和允许的行为。给定一组规则，重要的是机器人能够建立其规则，其基于感知的信念，其计划的行动及其后果之间的一致性。本文研究了机器人智能体如何使用模型检验来检验其规则、信念和动作的一致性。一个规则集是由一个布尔演化系统与同步语义，它可以被转换成一个标记的转换系统（LTS）。证明了稳定性和一致性可以表示为计算树逻辑（CTL）和线性时态逻辑（LTL）性质。提出了两种新的算法，分别进行实时一致性和稳定性检查。他们的实现为我们提供了一个计算工具，它可以形成有效的一致性检查的基础上，船上的机器人。
2016-11-10 cs.LO cs.RO
Horn-ICE Learning for Synthesizing Invariants and Contracts
Indian Institute of Science（印度科学学院）；Amazon India（亚马逊印度）；University of Illinois, Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）；Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）
我们设计了学习算法合成不变量使用霍恩蕴涵反例（霍恩ICE），扩展ICE学习模型。特别是，我们描述了一个决策树学习算法，学习霍恩ICE样本，工作在多项式时间，并使用统计算法来学习小树，满足样本。由于大多数验证证明可以使用Horn子句建模，Horn-ICE学习是一种更强大的技术，可以学习证明程序正确的归纳注释。我们的实验表明，我们的算法的实现是能够学习足够的归纳不变量和合同有效地为各种顺序和并发程序。
2017-12-26 cs.LG cs.LO cs.PL
Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
本文提出按需自动综合 catamorphisms 以表达 ADT 上 CHC 模型的框架，并实现 Catalia，实验显示其在可满足实例上优于现有求解器且支撑 ChocoCatalia 获奖。
2025-07-28 cs.LO
Solving Horn Clauses on Inductive Data Types Without Induction
基于归纳定义的数据结构，如列表和树，我们解决了约束Horn子句（CHC）的可满足性验证问题。我们提出了一种转换技术，其目标是删除这些数据结构的CHCs，从而减少其满足性的整数和布尔CHCs的可满足性问题。我们提出了一个转换算法，并确定了一类条款，它总是成功的。我们还考虑了该算法的扩展，它结合了子句转换与整数约束推理。通过实验评估，我们表明，我们的技术大大提高了Z3求解器的有效性，CHCs。我们还表明，我们的验证技术的基础上CHC转换，然后CHC解决方案，是有竞争力的CHC求解器与归纳扩展。本文件正在考虑被TPLP接受。
2018-04-24 cs.LO cs.PL
Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses
本文提出了一种基于规范自动转换的命令式程序正确性验证方法。给定一个程序prog，我们考虑形式为$\{φ\}$ prog $\{ψ\}$的部分正确性规范，其中断言$φ$和$ψ$是由可能递归的Horn子句的集合Spec定义的谓词，其前提中具有线性算术（LA）约束（也称为约束Horn子句）。验证方法包括在构造一组PC的约束Horn子句，其可满足性意味着$\{φ\}$ prog $\{ψ\}$是有效的。我们强调了一些限制的国家的最先进的约束霍恩子句求解方法，这里称为LA求解方法，证明可满足性的条款，通过寻找线性算术解释的谓词。特别是，我们证明了存在一些规格，不能证明有效的任何这些LA解决方法。这些规范要求证明一组包含非线性子句（即前提中有多个原子的子句）的受约束Horn子句的PC的可满足性。然后，我们提出了一个转换，称为线性化，PC转换成一组线性条款（即条款，在其前提中最多一个原子）。我们表明，几个规格，不能被证明是有效的LA解决方法，可以被证明是有效的线性化后。我们还提出了一种策略，用于执行线性化在一个自动的方式，我们报告的一些实验结果，通过使用我们的方法的初步实施。
2015-07-21 cs.LO cs.PL
Multiple Query Satisfiability of Constrained Horn Clauses
本文针对含多个查询的约束 Horn 子句可满足性问题，提出一种查询信息融合的变换技术，使新查询携带其他查询的相关信息，从而提升 CHC 求解算法对查询间关系的利用能力，并在列表和树等代数数据类型程序验证基准上验证了其有效性。
2024-01-11 cs.LO cs.PL cs.SE
Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System
本文提出面向广义 HFL 的依赖精化类型系统，并借助 CPS 编码与扩展 CHC 求解，以少量修改复用现有技术来验证高阶概率程序的多种定量性质。
2024-07-03 cs.LO
Transformational Verification of Quicksort
为约束逻辑程序开发的许多转换技术，也称为约束Horn子句（CHC），在程序验证领域中找到了新的有用的应用。在本文中，我们通过基于转换的验证方法进行了一个非平凡的案例研究。我们认为熟悉的Quicksort程序排序列表，写在一个功能性的程序设计语言，我们验证的前/后置条件，指定预期的正确性属性的功能中定义的程序。我们通过以下方式验证这些属性：（1）将它们转换为CHC，（2）通过删除所有列表出现来转换CHC，以及（3）通过使用布尔和整数的Eldarica求解器来检查转换后的CHC的可满足性。在第（2）点提到的转换需要对以前工作中提出的消除归纳定义的数据结构的算法进行扩展，因为在转换的一个阶段，我们使用在以前阶段已经证明的一些性质作为引理。
2020-08-07 cs.LO cs.PL
Source Code Verification for Embedded Systems using Prolog
系统相关的嵌入式软件需要可靠，因此需要经过良好的测试，特别是对于航空航天系统。验证程序的一种常用技术是分析程序的抽象语法树（AST）。树结构可以用逻辑程序设计语言Prolog来优雅地分析。此外，Prolog还为全面分析提供了进一步的优势：一方面，它本身提供了多功能选项来有效地处理树或图数据结构。另一方面，Prolog的非确定性和回溯简化了对程序流的不同变体的测试，而不需要付出很大的努力。一个基于规则的方法与Prolog允许验证目标的特点，在一个简洁和声明的方式。在本文中，我们描述了我们的方法来验证的闪存文件系统的源代码与Prolog的帮助。闪存文件系统是用C++编写的，专门为卫星使用而开发。我们将一个给定的抽象语法树的C++源代码转换成Prolog的事实，并推导出调用图和执行序列（树），然后进一步测试验证目标。由于控制结构的不同程序流分支是通过回溯作为完整执行序列的子树而导出的。最后，这些子树在Prolog中进行了验证。我们说明了我们的方法与案例研究，在那里我们搜索不正确的应用程序中使用的实时操作系统RODOS的嵌入式软件中的信号量。我们依赖于计算树逻辑（CTL），并设计了一个嵌入式领域特定语言（DSL）的Prolog来表达的验证目标。
2017-01-03 cs.LO cs.PL cs.SE
Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
我们解决的问题，验证程序的功能满足他们的合同，指定的前/后条件。我们遵循一种基于约束Horn子句（CHCs）的方法，通过该方法，验证问题被简化为检查来自给定程序和合同的一组子句的可满足性的问题。我们认为程序，操作代数数据类型（ADT）和一类合同指定的蜕变，即简单的递归模式定义的给定ADT的功能。我们通过几个例子表明，国家的最先进的CHC可满足性工具是不能有效地解决可满足性问题的合同直接翻译成CHCs。为了克服这个困难，我们提出了一种转换技术，删除ADT条款的CHCs和派生新的条款，工作在基本排序，如整数和布尔。因此，当使用衍生的CHC时，不需要关于ADT的归纳规则。我们证明了变换是合理的，也就是说，如果CHCs的导出集是可满足的，那么原来的集合也是可满足的。我们还证明了转换总是终止的合同指定的类的蜕变。最后，我们提出了我们的技术的实现时，验证许多非平凡的合同ADT操纵程序所获得的实验结果。
2022-09-07 cs.LO cs.PL
BPPChecker: An SMT-based Model Checker on Basic Parallel Processes(Full Version)
并发程序的程序验证是一个很大的挑战，由于一般的不可判定的结果。Petri网及其扩展在大多数工作中使用。然而，现有的基于Petri网的验证器很难是完整的和有效的。基本并行进程（BPP）作为Petri网的一个子类，可以作为描述和验证并发程序的模型，具有较低的复杂度。我们提出并实现了BPP的，第一个模型检查器，用于验证一个子类的CTL BPP。针对BPP的模型检验问题，提出了基于约束的算法，并用SMT求解器Z3处理公式。对于EF算子，我们将EF公式的模型检验归结为存在Presburger公式的可满足性问题。对于EG算子，我们给出了k步有界语义，并将EG公式的模型检验问题归结为线性整数运算的可满足性问题。此外，我们给演员通信系统（ACS）的过近似BPP的语义和评估BPP的演员通信系统从真正的Erlang程序生成。实验结果表明，BPPPERT在一系列Erlang程序的分支时间属性验证问题上比现有工具有更高的效率。
2021-10-25 cs.FL cs.LO
