Solving non-linear Horn clauses using a linear Horn clause solver
在本文中，我们表明，检查可满足性的一组非线性霍恩条款（也称为非线性霍恩条款计划）可以实现使用求解器的线性霍恩条款。我们实现这一点，通过交错的程序转换与线性霍恩条款（也称为线性霍恩条款求解器）的可满足性检查。程序转换是基于树维度的概念，我们将其应用于一组非线性子句，产生一组其派生树具有有界维度的集合。这样一套条款可以线性化。然后，主要的算法进行应用线性化变换和求解器的线性霍恩条款的一系列条款的连续增加的维度范围。然后，通过使用较低维度的条款解决方案来（部分）线性化较高维度的条款，进一步发展了该方法。我们构建了一个原型实现这种方法，并进行了一些实验上的一组验证问题，这表明了一些承诺。
2016-07-15 cs.LO cs.PL
ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses
本文提出加速驱动子句学习（ADCL）演算，利用循环加速避免递归 CHCs 在归结证明中的重复推导，从而缩短证明，并在 LoAT 中实现后与现有工具实证比较。
2023-07-14 cs.LO
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
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
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
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
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
Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types
余代数，霍恩子句逻辑编程和类型研讨会于2016年11月28日至29日在爱丁堡举行。该研讨会标志着EPSRC授予的类型推断的共代数逻辑编程的结束。Komendantskaya，赫瑞瓦特大学和J. Power，巴斯大学，英国。
2017-09-13 cs.LO cs.PL
Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
一阶解析已经被用于类型推断很多年了，包括Hindley- Milner类型推断、类型类和约束数据类型。依赖类型是函数式语言的一个新趋势。在本文中，我们证明相关的一阶分辨率可以发挥重要作用，在自动化类型推断和术语合成依赖类型的语言。我们提出了一个演算，翻译类型推断和长期合成问题，在依赖类型化的语言，一个逻辑程序和目标的证明相关的一阶霍恩子句逻辑。然后，计算出的答案替换和证明项为给定的类型推断和项合成问题提供解决方案。我们证明了我们的方法的可判定性和可靠性。该文件正在考虑被TPLP接受。
2018-04-30 cs.LO
Towards Coinductive Theory Exploration in Horn Clause Logic: Position Paper
Heriot-Watt University（赫瑞-瓦特大学）
在霍恩子句逻辑中，共归纳有两种形式：在自指性质和关系的证明中，以及在涉及（可能不规则的）无限数据的构造的证明中。这两种共归纳推理的证明都曾在文献中出现过，但缺乏对这两种证明及其关系的系统分析。我们提出了一个一般的证明理论框架，处理这两种共同归纳霍恩子句逻辑。为了这个目的，我们提出了一个共同归纳扩展米勒等人的框架统一证明，并证明其可靠性相对于共同归纳模型的霍恩子句逻辑。
2018-09-13 cs.AI 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
Initial Limit Datalog: a New Extensible Class of Decidable Constrained Horn Clauses
我们提出了初始极限数据库，一个新的可扩展类的约束霍恩条款的可满足性问题是可判定的。这个类可以被看作是一阶语言极限数据集$_Z$（数据集模线性整数运算的一个片段）的高阶逻辑（对类型有简单的限制）的推广，但是可以用任何合适的背景理论来实例化。例如，片段是可判定的任何可数良好的准序与可判定的一阶理论，如自然数向量下的分量线性算术，和有界的，上下文无关的语言的字排序的子字关系。在背景理论的某些假设下，初始极限公式的可满足性可以通过一种新的项模型来证明，我们称之为集合结构。虽然所有模型的集合通常是不可数的，但所有可枚举结构的集合是递归可枚举的，并且模型检验是可判定的。
2021-04-29 cs.LO
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
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
Coinductive Uniform Proofs
共归纳在霍恩子句逻辑中有两种形式：循环性质和关系的证明，以及涉及无限数据构造的证明。这两种共归纳推理的证明都曾在文献中出现过，但缺乏对这两种证明及其关系的系统分析。我们提出了一个一般的证明理论框架，处理这两种共同归纳霍恩子句逻辑。为此，我们提出了一个共同归纳的Miller等人的框架的统一证明，并证明其可靠性相对于共同归纳模型的霍恩子句逻辑。
2019-03-18 cs.LO
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
An iterative approach to precondition inference using constrained Horn clauses
我们提出了一种方法，用于自动推理的条件上的初始状态的程序，保证在程序中的安全断言不被违反。约束霍恩条款（CHCs）被用来建模的程序和断言在一个统一的方式，我们使用标准的抽象解释，得出一个过度近似的不安全的初始状态。前提条件则是对应于该集合的补集的约束，欠近似安全初始状态的集合。这种互补的想法并不新鲜，但以前试图利用它的尝试已经失去了精确性。在这里，我们开发了一种迭代专门化算法，以提供更精确的，在某些情况下最佳的安全条件。该算法结合了现有的转换，即约束专业化，部分评估和消除痕迹的转换。这些转换中的最后两个执行多变量专门化，从而导致提高精度的析取约束。该算法的实现和测试的基准套件的程序从文献中的前提推理和软件验证比赛。
2018-04-17 cs.LO
An encoding of array verification problems into array-free Horn clauses
自动验证程序的安全属性是困难的，如果程序作用于数组或其他形式的映射，则更难。存在许多方法来验证程序操作上的布尔和整数值（例如抽象的解释，反例引导的抽象细化使用插值），但转置它们数组属性已充满了困难。与大多数以前的方法相比，我们不引入一个新的抽象域或一个新的插值过程数组。相反，我们生成一个抽象的标量问题，并将其提供给一个预先存在的求解器，与可调precision.Our转换的问题表示使用霍恩条款，一个共同的格式与明确和明确的逻辑语义验证问题。我们的编码的一个重要特点是，它创建了一个非线性的霍恩问题，与树展开，即使下面的“平坦”的控制图结构通常会产生一个线性的霍恩问题，与线性展开。也就是说，我们的编码不能表示成另一个控制流图问题的编码，并真正利用霍恩子句格式的能力。我们说明了我们的方法与选择排序的功能正确性的完全自动化的证明。
2015-09-30 cs.LO cs.PL
Higher-Order Constrained Horn Clauses and Refinement Types
出于高阶函数程序自动验证中的应用，我们开发了一个概念的约束霍恩条款在高阶逻辑和决策问题，其可满足性。我们表明，虽然高阶子句的可满足系统一般不具有最小模型，有一个规范模型的概念，通过减少到一种单调逻辑程序的问题。在高阶程序验证的工作之后，我们开发了一个细化类型的系统，以推理和自动搜索模型。这为解决决策问题提供了一个合理但不完整的方法。最后，我们证明了一个扩展的决策问题，其中细化类型直接用作警卫存在量词可以减少到原来的问题。这个结果可以用来表明，高阶函数的性质，可定义使用细化类型也表示使用高阶约束霍恩子句。
2017-08-01 cs.LO cs.PL
Horn Clauses in Hybrid-Dynamic First-Order Logic
我们提出了一个混合动态一阶逻辑作为一个正式的基础，可重构系统的指定和推理。顾名思义，我们开发的形式主义扩展了（多排序）一阶逻辑，具有混合逻辑和动态逻辑所共有的特征。这为处理可重构系统提供了某些关键优势，例如：（a）名词的签名，包括操作和关系符号，允许引用特定的可能世界/系统配置-如在混合逻辑的情况下;（b）刚性和柔性符号的区别签名，其中刚性符号在可能世界中被统一解释;这就支持了严格的量化形式，确保变量具有相同的解释，而不管在哪个可能的世界中对其进行评估;（c）混合术语，在严格的符号背景下增加逻辑的表达能力;以及（d）动态逻辑动作上的模态运算符，其被定义为二元名义关系上的正则表达式。然后，我们研究霍恩条款在这个混合动态逻辑，并开发了一系列的结果，导致一个初始语义定理的任意条款集。这表明混合动态一阶逻辑的一个重要片段具有良好的计算特性，可以作为定义可重构系统的可执行语言的基础。最后，我们列出了逻辑编程的基础，在这个片段证明了混合动力的变种Herbrand定理，减少了语义蕴涵的逻辑编程查询的程序搜索一个合适的答案替代。
2019-05-10 cs.LO
Combining Forward and Backward Abstract Interpretation of Horn Clauses
前向分析和后向分析的交替是程序抽象解释中的一种标准技术，当我们希望证明某些不需要的程序状态不可达时，这种技术特别有用。当前用于组合Horn子句的前向（在逻辑编程术语中为自底向上）和后向（自顶向下）抽象解释的最先进技术是查询-应答转换。它转换了Horn子句系统，使得标准的前向分析可以从目标向前和向后传播约束。问答转换是有效的，但有我们希望解决的问题。为此，我们引入了一个新的后向收集语义，它适用于交替的前向和后向抽象解释的Horn子句。我们展示了如何交替可以用来证明无法达到的目标，以及如何每一个后续运行的分析产生一个完善的系统模型。实验上，我们观察到，结合向前和向后的分析是很重要的分析系统编码的问题，在C程序的可达性。特别是，遵循我们的新语义的组合提高了我们自己的抽象解释器的精度，包括与查询-答案转换系统的前向分析相比。
2017-08-07 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
Structural Resolution: a Framework for Coinductive Proof Search and Proof Construction in Horn Clause Logic
逻辑编程（LP）是一种基于一阶Horn子句逻辑的程序设计语言，它使用SLD-归结作为半决策过程。有限的SLD计算是归纳的声音和完整的最少Herbrand模型的逻辑程序。对偶地，SLD分解的共递归方法将无限SLD计算视为连续逼近程序的最大完全Herbrand模型中包含的无限项。在LP中实现协递归的最新算法基于循环检测。然而，这样的算法只支持推理的逻辑蕴涵合理的条款，他们没有考虑到生产力的重要性质，在无限的SLD计算。因此，循环检测落后于交互式定理证明（ITP）和项重写系统（TRS）中的共归纳方法。结构分解是一种新提出的替代SLD分解的方法，它可以定义和半决定一个适合于LP的生产力概念。在本文中，我们证明了健全的结构分辨率相对于Herbrand模型语义生产归纳，共归纳，混合归纳共归纳逻辑程序。我们介绍了两个算法，支持共归纳证明搜索无限生产条件。一个算法结合了循环检测的方法与生产性结构的解决方案，从而保证生产力的共归纳证明的无穷有理项。另一种则允许对无限非理性生产性术语的片段进行懒惰的合理观察。这使得LP中的共归纳方法与ITP和TRS中基于生产力的共归纳观察方法相提并论。
2017-05-04 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
Hierarchical State Machines as Modular Horn Clauses
在基于模型的开发中，嵌入式系统是使用一种混合的形式主义来建模的，它捕获了计算流，分层状态机捕获了系统的模态行为。对于安全性分析，现有的方法依赖于编译方案，该方案将原始模型（隐式和状态机）转换为纯隐式形式主义。这样的编译往往会导致重要的结构信息，捕捉系统的模态行为的损失。在以前的工作中，我们已经开发了一种编译技术，从一个模块化的Horn子句的形式主义。在本文中，我们提出了一种新的技术，忠实地编译成模块化的霍恩条款的层次状态机。我们的编译技术保留了系统的结构和模态行为，使这些模型的安全分析更容易处理。
2016-07-15 cs.LO cs.PL cs.SE
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
Analysis and Transformation of Constrained Horn Clauses for Program Verification
本文综述了最近的工作应用分析和转换技术，起源于约束逻辑编程（CLP）领域的问题，验证软件系统。我们提出了基于专业化的技术翻译验证问题，为不同的程序设计语言，并在一般的软件系统，到满足性问题的约束霍恩条款（CHCs），一个术语，已成为流行的验证领域，指CLP程序。然后，我们描述了静态分析技术的CHCs，可用于推断相关的程序属性，如循环不变。我们还概述了一些转换技术的基础上专业化和折叠/展开规则，这是有用的，以提高CHC可满足性工具的有效性。最后，我们讨论了应用这些技术的未来发展。
2021-08-02 cs.LO cs.PL
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
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
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 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
CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses
本文提出基于组合策略的CHC求解器CHCVERIF，复用成熟软件验证工具求解CHC问题，验证了该思路的可行性与潜力。
2025-10-30 cs.LO cs.PL cs.SE
Ultimate TreeAutomizer (CHC-COMP Tool Description)
我们提出了终极TreeAutomizer，一个求解器的约束Horn子句集的可满足性。约束Horn子句（CHC）是一阶逻辑的一个片段，在算法求解的表达性和可访问性方面具有吸引人的特性。Ultimate TreeAutomizer是基于轨迹抽象、树自动机和树插值技术的。本文作为CHC-COMP 2019中TreeAutomizer的工具描述。
2019-07-09 cs.LO
SLD-Resolution Reduction of Second-Order Horn Fragments -- technical report --
我们提出了SLD-决议，不可判定的问题，找到一个有限的子集的一组条款，从整个集合可以得出使用SLD-决议的推导减少问题。我们研究了二阶Horn逻辑的各种片段的约简，并在归纳逻辑程序设计中有具体的应用。我们还讨论了如何将这些结果扩展到标准分辨率。
2019-02-26 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
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
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
CHC-COMP 2023: Competition Report
本文介绍了第六届约束霍恩子句求解器竞赛CHC-COMP 2023的组织情况及结果，该竞赛包含七个求解器和六个赛道。
2024-04-23 cs.LO
Catamorphic Abstractions for Constrained Horn Clause Satisfiability
本文提出将含 catamorphism 的受限 Horn 子句转换为等可满足且不含 catamorphism 的子句集，从而无需扩展现有求解器即可验证 ADT 程序性质，并实验证明其显著提升 CHC 求解性能。
2024-08-13 cs.LO cs.PL
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
Symbolic Execution of Constrained Horn Clauses
TU Vienna（维也纳工业大学）；Uppsala University（乌普萨拉大学）；University of Regensburg（雷根斯堡大学）
本文研究约束 Horn 子句的符号执行，提出约束消解演算，统一前向与后向推理，证明完备性并开发剪枝准则，实验验证于 Eldarica 求解器。
2026-10-05 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
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
The Limits of Horn Logic Programs
给定Horn逻辑程序序列$\{Π_n\}$，$\{Π_n\}$的极限$Π$是这样的子句集合，使得$Π$中的每个子句属于几乎每个$Π_n$，并且无限多个$Π_n$中的每个子句也属于$Π$.极限程序$Π$仍然是Horn，但可能是无限的。本文考虑给定Horn逻辑程序序列$\{Π_n\}$的极限的最小Herbrand模型是否等于每个逻辑程序$Π_n$的最小Herbrand模型的极限。本文证明了这一性质一般不成立，但如果Horn逻辑程序满足一个可语法检验且可由一类Horn逻辑程序满足的假设，则这一性质成立。因此，在此假设下，我们可以通过每个有限程序$Π_n$的最小Herbrand模型序列来逼近极限$Π$的最小Herbrand模型.我们还证明了，如果一个有限Horn逻辑程序满足这个假设，那么这个程序的最小Herbrand模型是递归的。最后，利用动力系统的稳定性概念，证明了这一假设是保证Horn逻辑程序不动点稳定的充分条件。
2002-02-07 cs.LO cs.PL
