Higher-Order Constrained Horn Clauses and Refinement Types
出于高阶函数程序自动验证中的应用，我们开发了一个概念的约束霍恩条款在高阶逻辑和决策问题，其可满足性。我们表明，虽然高阶子句的可满足系统一般不具有最小模型，有一个规范模型的概念，通过减少到一种单调逻辑程序的问题。在高阶程序验证的工作之后，我们开发了一个细化类型的系统，以推理和自动搜索模型。这为解决决策问题提供了一个合理但不完整的方法。最后，我们证明了一个扩展的决策问题，其中细化类型直接用作警卫存在量词可以减少到原来的问题。这个结果可以用来表明，高阶函数的性质，可定义使用细化类型也表示使用高阶约束霍恩子句。
2017-08-01 cs.LO cs.PL
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
Combining Forward and Backward Abstract Interpretation of Horn Clauses
前向分析和后向分析的交替是程序抽象解释中的一种标准技术，当我们希望证明某些不需要的程序状态不可达时，这种技术特别有用。当前用于组合Horn子句的前向（在逻辑编程术语中为自底向上）和后向（自顶向下）抽象解释的最先进技术是查询-应答转换。它转换了Horn子句系统，使得标准的前向分析可以从目标向前和向后传播约束。问答转换是有效的，但有我们希望解决的问题。为此，我们引入了一个新的后向收集语义，它适用于交替的前向和后向抽象解释的Horn子句。我们展示了如何交替可以用来证明无法达到的目标，以及如何每一个后续运行的分析产生一个完善的系统模型。实验上，我们观察到，结合向前和向后的分析是很重要的分析系统编码的问题，在C程序的可达性。特别是，遵循我们的新语义的组合提高了我们自己的抽象解释器的精度，包括与查询-答案转换系统的前向分析相比。
2017-08-07 cs.LO cs.PL
Analysis and Transformation of Constrained Horn Clauses for Program Verification
本文综述了最近的工作应用分析和转换技术，起源于约束逻辑编程（CLP）领域的问题，验证软件系统。我们提出了基于专业化的技术翻译验证问题，为不同的程序设计语言，并在一般的软件系统，到满足性问题的约束霍恩条款（CHCs），一个术语，已成为流行的验证领域，指CLP程序。然后，我们描述了静态分析技术的CHCs，可用于推断相关的程序属性，如循环不变。我们还概述了一些转换技术的基础上专业化和折叠/展开规则，这是有用的，以提高CHC可满足性工具的有效性。最后，我们讨论了应用这些技术的未来发展。
2021-08-02 cs.LO cs.PL
Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses
我们建立证明理论，建设性和coalgebraic基础证明搜索共归纳霍恩条款理论。操作语义的共归纳霍恩子句决议铸造方面的共归纳统一的证明;其建设性的内容是通过相对于一个直观的一阶逻辑与递归控制后的模态的可靠性暴露;和可靠性的证明系统证明相对于一个新的共代数描述完整的Herbrand模型。
2022-03-15 cs.LO
Generalised Interpolation by Solving Recursion-Free Horn Clauses
在本文中，我们提出了InterHorn，无递归Horn子句的求解器。InterHorn的主要应用领域在于解决软件验证中出现的插值问题。我们展示了如何一系列的插值问题，包括路径，过渡，嵌套，状态/过渡和良好的插值可以直接由InterHorn处理。通过详细说明这些插值问题和他们的霍恩子句表示，我们希望鼓励出现一个共同的后端插值接口有用的不同的验证工具。
2014-12-03 cs.LO
Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report)
在软件验证的主要挑战之一是有效和精确的程序与过程和循环的组合分析。插值方法仍然是最有前途的技术之一，这样的验证，是密切相关的解决霍恩子句约束。我们引入了一个新的概念插值，析取插值，解决了更一般的一类问题，在一个步骤相比，以前的概念插值，如树插值或归纳序列的插值。我们目前的算法和复杂性建设的析取插值，以及它们的使用内的抽象细化循环。我们已经实现了霍恩条款验证算法，使用析取插值和评估他们的基准表示为霍恩条款的整数线性算术理论。
2013-01-21 cs.LO
Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning
本卷包含第三届程序等价和关系推理研讨会（PERR）和第六届验证与综合霍恩子句研讨会（HCVS）的联合后续会议记录，分别于4月6日和7日在捷克共和国布拉格举行，作为ETAPS的附属研讨会。
2019-07-08 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
Removing Unnecessary Variables from Horn Clause Verification Conditions
验证条件（Verification Conditions，VC）是一种逻辑公式，其可满足性保证了程序的正确性。我们认为VC的形式约束霍恩条款（CHC），这是自动生成的编码（解释器）的程序设计语言的操作语义。VC是通过基于展开/折叠变换规则的程序专门化而得到的，并且正如在专门化解释器时经常发生的那样，它们包含不必要的变量，即，在验证下的程序的正确性证明不需要的变量。在本文中，我们适应的CHC设置的一些技术，开发用于删除不必要的变量，从逻辑程序，我们表明，在某些情况下，这些技术的应用增加了霍恩子句求解器的有效性时，证明程序的正确性。
2016-07-15 cs.LO cs.PL cs.SE
Hierarchical State Machines as Modular Horn Clauses
在基于模型的开发中，嵌入式系统是使用一种混合的形式主义来建模的，它捕获了计算流，分层状态机捕获了系统的模态行为。对于安全性分析，现有的方法依赖于编译方案，该方案将原始模型（隐式和状态机）转换为纯隐式形式主义。这样的编译往往会导致重要的结构信息，捕捉系统的模态行为的损失。在以前的工作中，我们已经开发了一种编译技术，从一个模块化的Horn子句的形式主义。在本文中，我们提出了一种新的技术，忠实地编译成模块化的霍恩条款的层次状态机。我们的编译技术保留了系统的结构和模态行为，使这些模型的安全分析更容易处理。
2016-07-15 cs.LO cs.PL cs.SE
Symbolic Model Construction for Saturated Constrained Horn Clauses
针对饱和约束Horn子句缺乏可查询模型表示的问题，提出一种基于线性算术和无函数一阶语言的有效符号模型构造方法，能在有限时间内构造出可被有效评估的最小模型。
2023-07-24 cs.LO
Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates
我们解决的问题，证明约束角子句（CHCs）与代数数据类型（ADT），如列表和树的可满足性。我们提出了一种新的技术，用于将具有ADT的CHC转换为CHC，其中谓词仅定义在基本类型（如整数和布尔值）上。因此，我们的技术避免了在可满足性证明过程中明确使用归纳证明规则。对以前的ADT去除技术的主要扩展是一个新的转换规则，称为差分替换，它允许我们引入辅助谓词，对应于在进行归纳证明时经常需要的引理。我们提出了一个算法，使用新的规则，与传统的折叠/展开变换规则，自动删除ADT。我们证明了如果变换后的子句的集合是可满足的，那么原子句的集合也是可满足的。通过实验评估，我们表明，使用差分替换规则显着提高了ADT去除的有效性，我们表明，我们的基于变换的方法是有竞争力的一个完善的技术，扩展了CVC 4求解器与感应。
2020-10-01 cs.LO cs.PL
Satisfiability of Constrained Horn Clauses on Algebraic Data Types: A Transformation-based Approach
我们解决的问题，检查约束角子句（CHC）定义的代数数据类型（ADT），如列表和树的可满足性。我们提出了一种新的技术，用于将定义在ADT上的CHC转换为CHC，其中谓词的参数只有基本类型，如整数和布尔值。因此，我们的技术避免，在可满足性检查，明确使用的证明规则的基础上归纳的ADT。对以前的ADT去除技术的主要扩展是一个新的转换规则，称为差分替换，它允许我们引入辅助谓词，其定义对应于在进行归纳证明时使用的引理。我们提出了一个算法，执行自动删除ADT应用新的规则，连同传统的折叠/展开规则。我们证明了，在适当的假设下，转换条款的集合是可满足的当且仅当这样是原来的条款的集合。通过实验评估，我们表明，使用新的规则显着提高ADT删除的有效性。我们还表明，我们的方法是有竞争力的工具，使用归纳规则扩展CHC求解器。
2021-11-23 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
Reducing Higher-order Recursion Scheme Equivalence to Coinductive Higher-order Constrained Horn Clauses
高阶约束Horn子句（HoCHC）是高阶逻辑模理论的一个语义不变系统。HoCHC具有半判定背景理论上的半判定不可解性，适合于安全验证。关于它与更大类的高阶验证问题的关系，人们知之甚少。出于程序等价性的考虑，我们引入了一个共归纳版本的HoCHC，它具有最大的模型属性。我们将高阶递归方案（HoRS）的编码定义为HoCHC逻辑程序。这种编码的正确性降低了开放HoRS等价问题的可判定性-因此，LambdaY-演算Böhm树等价问题-在一个完整的可判定树理论上的共归纳HoCHC的半可判定性。
2021-09-10 cs.FL cs.LO cs.PL
Towards Coinductive Theory Exploration in Horn Clause Logic: Position Paper
Heriot-Watt University（赫瑞-瓦特大学）
在霍恩子句逻辑中，共归纳有两种形式：在自指性质和关系的证明中，以及在涉及（可能不规则的）无限数据的构造的证明中。这两种共归纳推理的证明都曾在文献中出现过，但缺乏对这两种证明及其关系的系统分析。我们提出了一个一般的证明理论框架，处理这两种共同归纳霍恩子句逻辑。为了这个目的，我们提出了一个共同归纳扩展米勒等人的框架统一证明，并证明其可靠性相对于共同归纳模型的霍恩子句逻辑。
2018-09-13 cs.AI cs.LO
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
ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses
本文提出加速驱动子句学习（ADCL）演算，利用循环加速避免递归 CHCs 在归结证明中的重复推导，从而缩短证明，并在 LoAT 中实现后与现有工具实证比较。
2023-07-14 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 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
Interpolant Tree Automata and their Application in Horn Clause Verification
本文研究了凸多面体域上的抽象解释与插值树自动机相结合的Horn子句验证的抽象-精化方案。这些技术以前已经单独应用，但在本文中以一种新的方式相结合。内插树自动机的作用是在精化过程中提供一个伪反例的概括，捕获一组可能无限的伪反例迹。在我们的方法中，这些痕迹，然后消除使用的Horn子句的变换。我们比较这种方法与其他两种方法，其中之一使用插值树自动机的算法跟踪抽象和细化，而另一个使用抽象的解释没有概括步骤的凸多面体的域。一些霍恩子句验证问题的实验结果的评价表明，插值树自动机与抽象解释的组合给出了一些增加的验证工具的力量，而有时会产生的性能开销。
2016-07-10 cs.LO
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
Catamorphic Abstractions for Constrained Horn Clause Satisfiability
本文提出将含 catamorphism 的受限 Horn 子句转换为等可满足且不含 catamorphism 的子句集，从而无需扩展现有求解器即可验证 ADT 程序性质，并实验证明其显著提升 CHC 求解性能。
2024-08-13 cs.LO cs.PL
Operational Semantics of Resolution and Productivity in Horn Clause Logic
本文研究了Horn子句逻辑中不同归结策略的运算性质和类型论性质。我们区分了四种不同的分辨率：统一分辨率（SLD分辨率），术语匹配分辨率，最近引入的结构分辨率和部分（或懒惰）分辨率。我们把它们统一表示为抽象的归约系统，这使我们能够对它们的性质进行彻底的比较分析。为了匹配这个小步骤的语义，我们建议霍华德的系统H作为一个类型理论的语义对应。使用系统H，我们将Horn公式解释为类型，并且将给定公式的推导解释为居住在公式给出的类型中的证明项。我们证明了这些抽象约简系统相对于系统H的可靠性，并证明了SLD-归结和结构归结相对于系统H的完备性。我们确定的条件下，结构分辨率在操作上相当于SLD分辨率。我们展示了没有存在变量的Horn子句程序的术语匹配解决方案与术语重写之间的对应关系。
2016-08-17 cs.LO
The Relationship between Craig Interpolation and Recursion-Free Horn Clauses
尽管经过数十年的研究，软件程序中仍然有许多常见的概念被认为对验证具有挑战性：其中包括并发性以及程序与过程的组合分析。作为一个有前途的方向，以克服这些困难，最近使用的Horn约束作为软件程序的中间表示已被提出。Horn约束与Craig插值有关，Craig插值是用于在验证中构造和细化抽象以及合成归纳循环不变量的主要技术之一。我们给出了一个调查的不同形式的克雷格插值在文献中发现，并表明，它们都对应于自然片段（递归自由）霍恩约束。我们还讨论了解决递归自由霍恩约束系统的技术。
2013-02-18 cs.LO
CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses
本文提出基于组合策略的CHC求解器CHCVERIF，复用成熟软件验证工具求解CHC问题，验证了该思路的可行性与潜力。
2025-10-30 cs.LO cs.PL cs.SE
Symbolic Execution of Constrained Horn Clauses
TU Vienna（维也纳工业大学）；Uppsala University（乌普萨拉大学）；University of Regensburg（雷根斯堡大学）
本文研究约束 Horn 子句的符号执行，提出约束消解演算，统一前向与后向推理，证明完备性并开发剪枝准则，实验验证于 Eldarica 求解器。
2026-10-05 cs.LO cs.PL
Clause Set Cycles and Induction
本文引入子句集循环形式体系，证明其包含于∃₁归纳理论但不包含于开放归纳理论，并推测两者不可比，最后将结果应用于n子句演算。
2020-11-27 cs.LO math.LO
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
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
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
A Fixed-point Theorem for Horn Formula Equations
我们考虑约束霍恩条款解决从更一般的角度来看，解决公式方程。约束Horn子句对应于Horn公式方程的子类。本文提出并证明了Horn公式方程的一个不动点定理，该定理基于将Horn子句集的极小模型在对象层次上的不动点计算表示为一阶逻辑中的公式，并给出了一个最小不动点算子.我们描述了这个不动点定理的几个推论，特别是关于程序验证的逻辑基础，并勾勒出如何概括它，将抽象的解释。
2021-09-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
Multiple Query Satisfiability of Constrained Horn Clauses
本文针对含多个查询的约束 Horn 子句可满足性问题，提出一种查询信息融合的变换技术，使新查询携带其他查询的相关信息，从而提升 CHC 求解算法对查询间关系的利用能力，并在列表和树等代数数据类型程序验证基准上验证了其有效性。
2024-01-11 cs.LO cs.PL 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
CTL* Verification and Synthesis using Existential Horn Clauses
Technion - Israel Institute of Technology（以色列理工学院）
本文提出基于存在性Horn子句（EHCs）的自动验证与合成方法，用于无限状态反应程序对CTL*规格的验证，展示了其在复杂系统中的应用。
2024-08-21 cs.LO
Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions
无递归约束Horn子句是一种逻辑规划问题，它可以用有界迭代和递归来描述程序的安全性。此外，许多CHC求解器将递归系统简化为一系列无递归的CHC系统，每个CHC系统都可以有效地求解。在本文中，我们定义了一类新的递归自由系统，名为子句依赖不相交（CDD），推广类定义在以前的工作。这个类的优点是，许多CDD系统比表示相同约束但属于不同类的系统小。这种规模上的优势使得CDD系统比其他类的同类系统更有效地解决问题。我们实现了一个名为Shara的CHC求解器。Shara通过减少一系列CDD系统的输入来解决任意CHC系统。我们的评估表明，在许多实际情况下，Shara优于最先进的实现。
2018-09-14 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
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
Lemma Generation for Horn Clause Satisfiability: A Preliminary Study
众所周知，命令式、函数式和逻辑程序的验证可以归结为约束Horn子句（CHC）的可满足性，并且这种可满足性检查可以通过使用CHC求解器（诸如Eldarica和Z3）来执行。这些求解器在处理简单的约束理论时表现良好，如线性代数和布尔理论，但当子句引用归纳定义的结构（如列表或树）上的约束时，它们的效率会大大降低。最近，我们提出了一种转换技术，用于消除那些归纳定义的数据结构，从而避免了将归纳原理纳入CHC求解器的需要。然而，这种技术可能会失败时，转换需要使用的lemmata的生成需要独创性。在本文中，我们通过一个例子，如何在转换CHCs消除归纳定义的结构的过程中，可以引入合适的谓词，称为差异谓词，其定义对应于引理被引入。通过第二个例子，我们表明，每当差异谓词不能介绍，我们可以介绍，而不是，辅助查询也对应于引理，这些引理的证明可以通过显示这些查询的可满足性。
2019-08-20 cs.LO cs.PL cs.SC
Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
一阶解析已经被用于类型推断很多年了，包括Hindley- Milner类型推断、类型类和约束数据类型。依赖类型是函数式语言的一个新趋势。在本文中，我们证明相关的一阶分辨率可以发挥重要作用，在自动化类型推断和术语合成依赖类型的语言。我们提出了一个演算，翻译类型推断和长期合成问题，在依赖类型化的语言，一个逻辑程序和目标的证明相关的一阶霍恩子句逻辑。然后，计算出的答案替换和证明项为给定的类型推断和项合成问题提供解决方案。我们证明了我们的方法的可判定性和可靠性。该文件正在考虑被TPLP接受。
2018-04-30 cs.LO
Collection analysis for Horn clause programs
我们考虑用数据结构包含的项的集合来近似它们。例如，列表，二叉树，元组等，可以近似为其中的项目的集合或多集合。这种近似可以用来提供逻辑程序的部分正确性。例如，人们可能希望指定，只要证明了原子$sort(t,s)$，则两个列表$t$和$s$包含相同的多项集（即，$s$是$t$的置换）。如果排序去除了重复项，则人们可能会推断$t$和$s$的基础项集合是相同的。如果这些结果可以静态和自动地确定，那么它们可能是有用的。我们提出了一个计划，这样的收集分析可以结构化和自动化。该方案的核心是使用线性逻辑作为Horn子句逻辑的计算逻辑。
2007-08-16 cs.LO
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
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
Initial Limit Datalog: a New Extensible Class of Decidable Constrained Horn Clauses
我们提出了初始极限数据库，一个新的可扩展类的约束霍恩条款的可满足性问题是可判定的。这个类可以被看作是一阶语言极限数据集$_Z$（数据集模线性整数运算的一个片段）的高阶逻辑（对类型有简单的限制）的推广，但是可以用任何合适的背景理论来实例化。例如，片段是可判定的任何可数良好的准序与可判定的一阶理论，如自然数向量下的分量线性算术，和有界的，上下文无关的语言的字排序的子字关系。在背景理论的某些假设下，初始极限公式的可满足性可以通过一种新的项模型来证明，我们称之为集合结构。虽然所有模型的集合通常是不可数的，但所有可枚举结构的集合是递归可枚举的，并且模型检验是可判定的。
2021-04-29 cs.LO
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
Coinductive Uniform Proofs
共归纳在霍恩子句逻辑中有两种形式：循环性质和关系的证明，以及涉及无限数据构造的证明。这两种共归纳推理的证明都曾在文献中出现过，但缺乏对这两种证明及其关系的系统分析。我们提出了一个一般的证明理论框架，处理这两种共同归纳霍恩子句逻辑。为此，我们提出了一个共同归纳的Miller等人的框架的统一证明，并证明其可靠性相对于共同归纳模型的霍恩子句逻辑。
2019-03-18 cs.LO
An iterative approach to precondition inference using constrained Horn clauses
我们提出了一种方法，用于自动推理的条件上的初始状态的程序，保证在程序中的安全断言不被违反。约束霍恩条款（CHCs）被用来建模的程序和断言在一个统一的方式，我们使用标准的抽象解释，得出一个过度近似的不安全的初始状态。前提条件则是对应于该集合的补集的约束，欠近似安全初始状态的集合。这种互补的想法并不新鲜，但以前试图利用它的尝试已经失去了精确性。在这里，我们开发了一种迭代专门化算法，以提供更精确的，在某些情况下最佳的安全条件。该算法结合了现有的转换，即约束专业化，部分评估和消除痕迹的转换。这些转换中的最后两个执行多变量专门化，从而导致提高精度的析取约束。该算法的实现和测试的基准套件的程序从文献中的前提推理和软件验证比赛。
2018-04-17 cs.LO
Horn Clauses in Hybrid-Dynamic First-Order Logic
我们提出了一个混合动态一阶逻辑作为一个正式的基础，可重构系统的指定和推理。顾名思义，我们开发的形式主义扩展了（多排序）一阶逻辑，具有混合逻辑和动态逻辑所共有的特征。这为处理可重构系统提供了某些关键优势，例如：（a）名词的签名，包括操作和关系符号，允许引用特定的可能世界/系统配置-如在混合逻辑的情况下;（b）刚性和柔性符号的区别签名，其中刚性符号在可能世界中被统一解释;这就支持了严格的量化形式，确保变量具有相同的解释，而不管在哪个可能的世界中对其进行评估;（c）混合术语，在严格的符号背景下增加逻辑的表达能力;以及（d）动态逻辑动作上的模态运算符，其被定义为二元名义关系上的正则表达式。然后，我们研究霍恩条款在这个混合动态逻辑，并开发了一系列的结果，导致一个初始语义定理的任意条款集。这表明混合动态一阶逻辑的一个重要片段具有良好的计算特性，可以作为定义可重构系统的可执行语言的基础。最后，我们列出了逻辑编程的基础，在这个片段证明了混合动力的变种Herbrand定理，减少了语义蕴涵的逻辑编程查询的程序搜索一个合适的答案替代。
2019-05-10 cs.LO
Verifying Solutions to Semantics-Guided Synthesis Problems
研究SemGuS框架下程序验证的求解器无关方法，通过将验证问题归约为`CLP演算查询有效性，提出改进框架并实现验证器，成功解决以往无法编码和综合的实例。
2025-04-06 cs.LO cs.PL
Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying
Comon和Cortier使用一阶子句的新类$\mathcal C$定义并建模了具有单盲复制的密码协议。他们在3-DEXPTIME中证明了它的可满足性问题。我们改进了这一结果表明，满足这个类是NEXPTIME完全的，使用新的分辨率技术。我们证明了满足是DEXPTIME完整的，如果条款是霍恩，这是所需的建模加密协议。虽然翻译霍恩条款只给出了一个DEXPTIME上界的保密问题，这些协议，我们进一步表明，这个保密问题实际上是DEXPTIME完全的。
2005-11-03 cs.CR cs.LO
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
Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
本文提出按需自动综合 catamorphisms 以表达 ADT 上 CHC 模型的框架，并实现 Catalia，实验显示其在可满足实例上优于现有求解器且支撑 ChocoCatalia 获奖。
2025-07-28 cs.LO
