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
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
Big-step and small-step Horn clause derivations applied to operational semantics
Roskilde University（罗斯基勒大学）；IMDEA Software Institute（IMDEA软件研究所）；Universidad Politécnica de Madrid (UPM)（马德里理工大学）；Spanish Council for Scientific Research (CSIC)（西班牙国家研究委员会）
本文证明Horn子句的大步推导与两种小步推导等价，并通过特化解释器将任意Horn子句集转换为等价子句集，实现编程语言大步语义到小步语义的转换。
2026-06-23 cs.PL
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
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
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
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
Defunctionalization of Higher-Order Constrained Horn Clauses
在可满足性模理论（SMT）成功的基础上，Bjørner等人发起了一项研究计划，提倡将Horn约束作为自动程序验证的合适基础。一阶约束Horn子句的概念最近被CathcartBurn等人扩展到高阶逻辑。为了利用SMT求解的显着效率，解决高阶Horn约束系统的一种自然方法是将它们减少到一阶Horn约束系统。本文提出了一种去功能化算法来实现约简。给定一个有序高阶约束Horn子句（HoCHC）问题实例，去功能化算法构造一个一阶有序约束Horn子句问题.除了良好的排序算法的输出，我们证明，如果一个输入HoCHC是可解的，那么它的defunctionalization的结果是可解的。反过来也成立，我们证明了使用最近的结果HoCHC的连续语义。据我们所知，这种去功能化算法是第一个健全的和完整的减少从系统的高阶霍恩约束系统的一阶霍恩约束。我们已经构建了DefMono，这是去功能化算法的原型实现。它首先将输入HoCHC问题去功能化，然后将结果馈送到后端SMT求解器。我们已经评估了DefMono经验的性能与其他两个高阶验证工具进行比较。
2019-02-22 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
Catamorphic Abstractions for Constrained Horn Clause Satisfiability
本文提出将含 catamorphism 的受限 Horn 子句转换为等可满足且不含 catamorphism 的子句集，从而无需扩展现有求解器即可验证 ADT 程序性质，并实验证明其显著提升 CHC 求解性能。
2024-08-13 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
Symbolic Execution of Constrained Horn Clauses
TU Vienna（维也纳工业大学）；Uppsala University（乌普萨拉大学）；University of Regensburg（雷根斯堡大学）
本文研究约束 Horn 子句的符号执行，提出约束消解演算，统一前向与后向推理，证明完备性并开发剪枝准则，实验验证于 Eldarica 求解器。
2026-10-05 cs.LO cs.PL
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
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
Automating Induction for Solving Horn Clauses
在各种范式（如命令式，逻辑，并发，功能和面向对象的）编写的程序的验证问题，可以减少到解决的问题，表示未知的归纳不变量的谓词变量的Horn子句约束。提出了一种基于归纳定理证明的Horn约束求解方法：该方法将Horn约束求解归结为对带有归纳谓词的一阶公式进行有效性检验，然后对谓词的推导进行归纳检验.为了自动化归纳证明，我们引入了一个新的证明系统，适合霍恩约束求解，并使用SMT求解器来履行证明搜索中产生的证明义务。所提出的方法的主要优点是，它可以验证关系规范在各种范式的程序中，多个函数调用需要同时进行分析。这类规范包括实际重要的规范，例如函数等价性、结合性、交换性、分配性、单调性、幂等性和非干扰性。此外，我们的新组合的霍恩子句约束与归纳定理证明，使我们能够自然和自动公理化递归函数，可能是非终止的，非确定性的，高阶的，异常提升，并在非归纳定义的数据类型。我们已经实现了一个关系验证工具的OCaml函数式语言的基础上所提出的方法，并在初步实验中取得了可喜的成果。
2016-10-21 cs.PL
Analysis and Transformation Tools for Constrained Horn Clause Verification
已经开发了几种技术和工具，用于验证表示为Horn子句的属性，并在背景理论（CHC）上进行约束。目前的CHC验证工具实现复杂的算法，往往局限于某些子类的CHC问题。我们在这项工作中的目的是调查使用的组合现成的技术从文献中的约束逻辑程序（CLP）的分析和改造，以解决具有挑战性的CHC验证问题。我们发现，许多问题可以解决使用的工具组合的基础上众所周知的技术，从抽象的解释，语义保持转换，程序专业化和问答转换。这提供了深入了解的自动，更一般的CHC验证工具的基础上的组件库的设计。
2014-05-15 cs.PL
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
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
Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses
本文提出一种结合自动机和逻辑的自动验证技术，通过knitted-tree编码将程序执行映射为单一树结构，并利用约束Horn子句刻画其组合性质，将验证简化为求解CHC可满足性问题，广泛适用于树操作程序的多种验证任务。
2024-10-12 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
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
Horn Clauses as an Intermediate Representation for Program Analysis and Transformation
许多最近的分析传统的命令式程序开始转换程序到逻辑程序，利用现有的LP分析和简单的LP语义。我们建议在整个编译过程中使用逻辑程序作为中间程序表示。通过确保确定性和单模性的限制，逻辑程序可以很容易地转换为机器语言或其他低级语言，同时保持简单的语义，使其适合作为程序分析和转换的语言。我们提出了一个简单的LP语言，强制执行确定性和单模性，并表明它使一个方便的程序表示的分析和转换。
2015-07-21 cs.PL
Solving Constrained Horn Clauses over ADTs by Finite Model Finding
一阶逻辑是一种表达计算属性的自然方式，传统上用于各种程序逻辑中，用于表达正确性属性和证书。随后，现代方法在自动推理的程序不变量的进展，对建设一阶可定义的不变量。虽然一阶表示对于某些理论来说是非常有表现力的，但是它们不能表达代数数据类型（ADT）的许多有趣的性质。因此，我们建议定期表示程序不变量与树自动机。我们展示了如何自动推断这样的规则不变量ADT操纵程序使用有限的模型发现。我们已经实现了我们的方法，并评估它对最先进的引擎的不变推理，在一阶逻辑ADT操纵程序。我们的评估表明，基于自动机的表示的不变量是更实际的一阶逻辑的基础上，因为不变量能够表达更复杂的计算属性和他们的自动建设是更便宜的。
2021-11-01 cs.PL
Verifying Solutions to Semantics-Guided Synthesis Problems
研究SemGuS框架下程序验证的求解器无关方法，通过将验证问题归约为`CLP演算查询有效性，提出改进框架并实现验证器，成功解决以往无法编码和综合的实例。
2025-04-06 cs.LO cs.PL
From Big-Step to Small-Step Semantics and Back with Interpreter Specialisation
我们调查表示的强制性程序作为约束霍恩条款。从操作语义转换规则开始，我们着手编写解释器作为受约束的霍恩子句程序直接编码的规则。然后，我们专门一个解释器相对于一个给定的源程序，以实现编译的源语言霍恩条款（第一个二村投影的实例）。该过程是详细描述了一个解释器的一个子集的C语言，直接编码的大步骤操作语义的规则。类似的翻译基于小步语义可以进行，但我们展示了一种方法来获得一个小步表示使用线性解释器大步霍恩条款。该解释器再次专门用于实现从大步到小步风格的翻译。使用第三个解释器可以将线性小步程序转换回大步非线性程序。使用Tarjan算法计算线性规划的正则路径表达式，然后该正则表达式引导解释器计算程序路径。在所有的转换阶段，我们使用一个既定的部分评估器和利用标准的逻辑程序转换，以消除冗余的数据结构和参数的谓词和重命名的谓词，以明确其链接到原始源程序中的语句。
2020-08-07 cs.LO cs.PL cs.SC
Constraint-based Relational Verification
近年来，他们已经有许多作品，旨在自动化关系验证。同时，尽管约束Horn子句（CHC）赋予了广泛的验证技术和工具，但它们缺乏表达$k$之外的超属性的能力-安全性，如广义非干扰和共同终止。本文介绍了一种新的和全自动的基于约束的关系验证方法。我们首先介绍了一类新的谓词约束满足问题称为pfwCSP的约束表示为子句模一阶理论的谓词变量的三种：普通的，良好的基础，或功能。这种对CHC的推广允许任意的（即，可能非Horn）子句、良好基础约束、功能约束，并且能够表达这些关系验证问题。我们的方法使我们能够表达和自动验证需要非平凡的问题实例（即，非顺序和非锁步）自合成，这是通过自动推断适当的指示何时以及哪个程序副本移动的指示符（或对齐）来实现的。为了解决这个新的语言中的问题，我们提出了一个约束求解方法pfwCSP的基础上分层反例引导归纳合成（CEGIS）的普通，良好的基础，和功能谓词。我们已经实现了所提出的框架，并取得了可喜的成果，在不同的关系验证问题，超出了以前的验证框架的范围。
2021-06-04 cs.LO cs.PL
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
Higher-Order MSL Horn Constraints
一元浅线性（MSL）类是一阶Horn子句的可判定片段，在世纪之交被发现和重新发现，在静态分析和验证中有应用。我们提出了一类新的高阶Horn约束，将MSL扩展到高阶逻辑，并开发了一个基于分辨率的决策过程。高阶MSL Horn约束可以很自然地捕获高阶程序中可能存在的调用和返回的复杂模式，这使得它们非常适合高阶程序验证。事实上，我们证明了高阶MSL可满足性问题和HORS模型检验问题是可互约的，因此高阶MSL可以被视为高阶模型检验的基于约束的方法。最后，我们描述了我们的决策过程及其应用程序验证套接字编程的实现。
2022-10-26 cs.PL
