foetus -- Termination Checker for Simple Functional Programs
本研究提出带终止性检查器的函数式语言foetus，通过提取函数调用、补全调用图并寻找参数良基结构序，来证明简单函数式程序的终止性。
2024-07-09 cs.LO cs.PL
Termination Analysis of General Logic Programs for Moded Queries: A Dynamic Approach
逻辑程序的终止问题可以用静态或动态的方法来解决。静态方法在编译时执行终止分析，而动态方法通过应用循环检查技术来表征和测试逻辑程序的终止。在本文中，我们提出了一种新的动态方法，终止分析一般逻辑程序与模态查询。我们解决了几个有趣的问题，包括如何制定一个SLDNF派生的moded查询，如何表征一个无限的SLDNF派生的moded查询，以及如何应用循环检查机制，以削减无限的SLDNF派生的终止分析的目的。所提出的方法非常强大和有用。它可以用来（1）测试一个逻辑程序是否终止于一个给定的具体或模态查询，（2）测试一个逻辑程序是否终止于所有的具体或模态查询，以及（3）找到所有（最一般的）最有可能终止（或非终止）的具体/模态查询。
2005-12-14 cs.LO cs.PL
Polytool: polynomial interpretations as a basis for termination analysis of Logic programs
我们的目标是研究移植终止分析技术开发的一个编程范式到另一个范式的可行性。在本文中，我们将展示如何适应终止分析技术的多项式解释的基础上-非常有名的术语重写系统（TRS）的背景下-获得新的（非转换）的终结分析技术，明确的逻辑程序（LP）。这导致了一种方法，可以被看作是一个直接推广的传统技术在终止分析的LP，线性规范和水平映射。我们的扩展一般化这些任意多项式。我们扩展了一些标准的概念和结果终止分析的上下文多项式的解释。我们还提出了一个基于约束的方法自动生成多项式的解释，满足终止条件。基于这种方法，我们实现了一个新的工具，称为Polytool，自动终止分析的LP。
2009-12-22 cs.LO cs.PL
Modular Verification for Almost-Sure Termination of Probabilistic Programs
在这项工作中，我们考虑几乎肯定终止问题的概率程序，询问是否一个给定的概率程序终止概率为1。可伸缩的程序分析方法通常依赖于模块化作为其理论基础。在非概率程序中，Floyd-霍尔逻辑的经典变式规则（V-规则）为模块化分析提供了基础。将该规则扩展到概率程序的几乎确定终止是相当棘手的，并且在[Fioriti and Hermanns 2015]中提出了一个概率变体。虽然所提出的概率变量谨慎地解决了可积性的关键问题，我们表明，所提出的模块化规则仍然是不健全的几乎肯定终止的概率程序。除了建立以前的规则的不健全，我们的贡献如下：首先，我们提出了一个健全的模块规则几乎确定终止的概率程序。我们的方法是基于一个新的概念下降上鞅。其次，对于算法方法，我们考虑下降上鞅是线性的，并表明它们可以在多项式时间合成。最后，我们提出了各种基准测试和几个自然的例子，模拟各种类型的嵌套而循环的概率程序的实验结果，并证明我们的方法是能够有效地证明其几乎肯定的终止属性。
2019-08-12 cs.LO cs.PL
KoAT: Automatic Complexity and Termination Analysis of Integer Programs
RWTH Aachen University（亚琛工业大学）
提出KoAT工具，通过交替模块化推断程序部分的运行时和大小上界，结合多种技术分析子程序，实现整数程序的复杂度界自动推断与终止性证明。
2026-06-26 cs.LO cs.PL
On Probabilistic Termination of Functional Programs with Continuous Distributions
本文研究了高阶概率函数程序的终止问题，包括递归、随机条件和连续分布抽样。关于具有连续分布的程序的终止概率的推理是困难的，因为终止执行的枚举不能提供任何非平凡的界限。我们提出了一个新的操作语义的基础上的痕迹的间隔，这是健全的和完整的标准采样为基础的语义，其中（可数）枚举可以提供任意紧的下限。因此，我们得到的第一个证明，决定几乎必然终止（AST）的程序连续分布是$Π^0_2$ -完全的。我们还提供了一个组合表示我们的语义的交叉类型系统。在第二部分中，我们提出了一种证明非仿射程序的AST的方法，即，递归程序，可以在递归体的计算期间，从不同的调用位置进行多次递归调用（一阶函数）。与确定性语言不同，递归调用站点的数量对终止概率有直接影响。我们的框架支持一个证明系统，可以验证AST的程序远远超出了现有方法的范围。我们已经构建了原型实现我们的方法计算下限的终止概率，AST验证。
2021-04-11 cs.LO cs.PL
Non-termination Analysis of Logic Programs with Integer arithmetics
在过去的几年中，分析器已被引入到检测类的非终止查询的明确的逻辑程序。虽然这些非终止性分析器已经被证明是相当精确的，但它们在现实生活中的Prolog程序上的适用性是有限的，因为大多数Prolog程序使用非逻辑功能。作为分析Prolog程序的第一步，本文给出了含整数运算的逻辑程序的不可终止条件。该分析仪基于我们在ICLP 2009上展示的非终止分析仪。分析从一类查询开始，并推断出一个子类的非终止的。在第一阶段，我们忽略算术运算的结果（成功或失败），假设所有算术调用都成功。在第二阶段中，我们成功的算术调用的特点作为一个约束问题，其解决方案确定的非终止查询。
2011-09-15 cs.LO cs.PL
Verifying Termination and Error-Freedom of Logic Programs with block Declarations
我们提出了延迟声明的逻辑程序的验证方法。验证的性质是终止和自由的错误有关的内置。关于终止，我们提出了两种方法。第一种方法试图消除众所周知的推测性输出绑定问题。第二种方法是基于识别的谓词，使用这个谓词的原子的文本位置是无关的终止。这项工作有三个特点：它允许在几种模式下使用谓词;它表明块声明，这是一个非常简单的延迟结构，足以确保所需的属性;它考虑到选择规则，假设它是在大多数Prolog实现。这些方法可用于验证现有程序和帮助编写新程序。
2000-06-23 cs.LO cs.PL
A Dynamic Approach to Characterizing Termination of General Logic Programs
本文给出了一般逻辑程序终止性的一个新的刻画。大多数现有的终止分析方法依赖于关于逻辑程序的源代码的结构的一些静态信息，诸如模式/类型、范数/级别映射、模型/参数间关系等。我们提出了一个动态的方法，它采用了一些关键的动态功能的无限（广义）SLDNF衍生，如重复选定的子目标和递归增加长期的大小。我们还介绍了一种新的制定SLDNF树，称为广义SLDNF树。广义SLDNF-树以与Prolog相同的方式处理负子目标，并且存在于任何一般逻辑程序中。
2002-04-12 cs.LO cs.PL
Termination Prediction for General Logic Programs
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所计算机科学国家重点实验室）；Department of Computer Science, Celestijnenlaan 200 A, B-3001 Heverlee, Belgium（计算机科学系）
我们提出了一个启发式的框架攻击的不可判定终止问题的逻辑程序，作为一种替代目前的终止/非终止证明方法。我们引入了终止预测的思想，它预测终止的逻辑程序的情况下，无论是终止或非终止证明是适用的。我们建立了一个必要和充分的表征无限（广义）SLDNF-衍生任意（具体或moded）查询，并开发了一个算法，预测终止一般逻辑程序与任意非floundering查询。我们已经实现了一个终止预测工具，并取得了相当满意的实验结果。除了5个程序打破了实验时间限制，我们的预测是100%正确的所有296个基准程序的终止竞争2007年，其中18个程序不能证明任何现有的国家的最先进的分析仪，如AProVE 07，NTI，Polytool和TALP。
2009-05-13 cs.AI cs.LO cs.PL
Termination Analysis of Linear-Constraint Programs
Complutense University of Madrid（马德里康普顿斯大学）；Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）；University of Oxford（牛津大学）
本文综述了线性约束程序终止分析的技术，涵盖可判定性结果、排名函数和非终止见证等方法，探讨了不同方法在表达力与计算复杂性间的权衡。
2026-07-27 cs.LO cs.PL
Automated Termination Proofs for Logic Programs by Term Rewriting
RWTH Aachen（亚琛工业大学）；TU Eindhoven（埃因霍温理工大学）；University of Innsbruck（因斯布鲁克大学）
逻辑程序的可终止性分析有两种方法：“转换”法和“直接”法。直接方法直接在逻辑程序的基础上证明终止。转换方法将一个逻辑程序转换成一个项重写系统（TRS），然后分析所得到的TRS的终止。因此，转换方法使以前为TRS开发的所有方法也可用于逻辑程序。然而，大多数现有的转换的适用性是相当有限的，因为它们只能用于逻辑程序的某些子类。(Most它们中的一个仅限于模式良好的程序。）在本文中，我们改进这些转换，使它们成为适用于任何明确的逻辑程序。为了用TRS模拟逻辑程序的行为，我们稍微修改了重写的概念，允许无限项。我们表明，我们的转换结果TRS这确实是适合自动终止分析。与大多数其他逻辑程序的终止方法相比，我们的技术也适用于逻辑程序设计，而不需要发生检查，这是在实践中通常使用的。我们在终止证明程序AProVE中实现了我们的方法，并在大量示例中成功地对其进行了评估。
2008-09-01 cs.AI cs.LO cs.PL
Termination Analysis for the $π$-Calculus by Reduction to Sequential Program Termination
我们提出了一个自动化的方法来证明终止的$π$演算过程，减少终止顺序程序的基础上：我们翻译一个$π$演算过程的顺序程序，使后者的终止意味着前者。然后，我们可以使用现成的终止验证工具来检查顺序程序的终止。我们的方法部分受到了邓和Sangiorgi对$π$演算的终止分析的启发，并通过将这样的通信链转换为目标顺序程序中的递归函数调用链，来检查复制输入通道上是否存在无限的通信链。我们已经实现了一个自动化的工具，所提出的方法的基础上，并确认其有效性。
2021-09-01 cs.PL
Almost-Sure Termination by Guarded Refinement
本文提出Caliper，一种基于受保护递归和概率耦合的高阶分离逻辑，通过证明程序与简单模型间的精化来建立概率程序的几乎必然终止，并在Coq中验证多个示例。
2024-11-11 cs.LO cs.PL
Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling
在逻辑编程中，动态调度是指在运行时确定每个解析（计算）步骤中原子的选择的情况，而不是像Prolog中从左到右的选择规则。这在例如并行编程中具有应用。在现有的语言中，以延迟声明的形式提供了一种控制动态调度的机制。在抽象技术细节的同时，引入了消耗输入的推导来描述动态调度。在本文中，我们首先正式延迟声明和输入消费派生之间的关系，在许多情况下，一对一的对应关系。然后，我们定义了一个模型理论的语义输入消费派生的简单模式的程序。最后，对于这类程序，我们提供了一个终止的充分必要条件。
2001-01-23 cs.LO cs.PL
Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs
本文研究了实变量概率规划的终止性问题。有关问题是：1.定性问题，询问（i）程序是否以概率1终止（几乎肯定终止）和（ii）预期终止时间是否有限（有限终止）; 2.定量问题，要求（i）近似预期的终止时间（期望问题）和（ii）计算边界B，使得在B步后终止的概率呈指数下降（浓度问题）。为了解决这些问题，我们利用排序上鞅的概念，这是一个强大的方法来证明概率程序的终止性。详细地说，我们专注于算法合成的线性排名上鞅仿射概率程序（APP）与天使和恶魔的非决定性。APP的一个重要子类是LRAPP，它被定义为所有APP的类，其上存在线性秩上鞅。我们的主要贡献如下。首先，我们证明了LRAPP的成员问题（i）可以决定在多项式时间的APP的最恶魔的非确定性，和（ii）是NP-困难的，在PSPACE的APP的天使的非确定性;此外，NP-困难的结果已经成立APP的没有概率和恶魔的非确定性。其次，我们证明了LRAPP的浓度问题可以解决在相同的复杂性LRAPP的成员问题。最后，我们证明了LRAPP上的期望问题可以在2 EXPTIME中求解，并且即使对于没有概率和非确定性的APP也是PSPACE困难的（即，确定性程序）。我们的实验结果表明，我们的方法来回答定性和定量的问题在APP的最恶魔的非决定论的有效性。
2015-10-28 cs.LO cs.PL
Inferring Termination Conditions for Logic Programs using Backwards Analysis
本文主要研究保证逻辑程序终止的模式的推理。这概括了传统的端接分析，其中分析仪试图验证指定模式的端接。我们的贡献是一种方法，其中传统的终止分析的组成部分相结合，向后分析，以获得终止推理的分析。我们确定了一个条件的组件的分析，保证终止推理将推断出所有的模式，可以检查终止。这种方法的应用，以提高传统的终止分析，也终止推理进行演示。
2003-12-12 cs.PL
Characterization of Termination for Linear Loop Programs
给出了线性齐次规划终止的充分必要条件。我们还开发了一个完整的方法来检查这类程序的终止性。我们的完整表征终止这样的程序是基于线性代数方法。我们减少了验证的终止问题，以检查一个确定的向量空间和一定的向量，都涉及到程序中的循环的正交性。此外，我们提供的理论结果和象征性的计算方法，保证的合理性，完整性和数值稳定性的方法。最后，我们表明，它是足够的解释变量值在一个特定的可数数域，甚至在其环的整数，当一个人想要检查终止的实数。
2014-09-10 cs.PL
Non-termination of Dalvik bytecode via compilation to CLP
我们提出了一套规则编译Dalvik字节码程序到一个逻辑程序与数组约束。结果程序的非终止性包含了原程序的非终止性，因此我们以前提出的证明约束逻辑程序的非终止性的方法也可用于证明Dalvik程序的非终止性.
2014-12-10 cs.PL
Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types
类型系统以组合的方式证明程序属性。从一个更大的程序中，可以抽象出一个部分，并通过使用被抽象出的部分的类型来证明所得到的抽象程序的属性。终止性和生产力是非平凡的，但所需的程序属性，并已提出了几个类型系统，保证终止，组成。这些类型系统与通过顺序迭代定义的最小和最大不动点密切相关。虽然大多数类型系统使用常规迭代，但我们在本文中考虑膨胀迭代。我们演示了这是如何导致一个更有原则的类型系统，递归基于有理有据的归纳。该类型系统有一个原型实现，MiniAgda，我们特别展示了它如何证明生产力的correcursive和混合递归correcursive功能。
2012-02-16 cs.LO cs.PL
Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs
概率程序用实值随机变量和随机分支扩展了经典的命令式程序。这类程序最基本的活性属性是终止属性。定性（也称为几乎肯定）终止问题给出了一个概率程序，询问程序是否以概率1终止。虽然排序函数为非概率规划提供了一个合理而完整的方法，但将其扩展到概率规划是通过排序上鞅（RSM）实现的。虽然已经建立了深入的理论成果，他们的应用程序与非确定性的概率程序仅限于学术的例子。对于非概率程序，字典排序函数提供了一个组成和实际的方法，终止分析现实世界的程序。在这项工作中，我们介绍字典的RSM，并表明他们提出了一个健全的方法几乎肯定终止的概率程序与非确定性。我们表明，字典的RSM提供了一个工具，组合推理几乎肯定终止，和线性算术的概率程序，他们可以有效地合成（在多项式时间）。我们还表明，与其他限制，甚至可以通过字典的RSM得到预期的终止时间的渐近界。最后，我们提出的实验结果抽象的真实世界的程序来证明我们的方法的有效性。
2017-09-12 cs.PL
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs
我们提出了TaDA现场，一个并发分离逻辑的推理组合终止阻塞细粒度并发程序。关键的挑战是如何处理抽象的原子阻塞：也就是说，抽象的原子操作具有阻塞行为，这些阻塞行为来自于例如细粒度自旋锁中的忙等待模式。我们的基本创新是抽象规范的设计，捕捉这种阻塞行为作为对环境的活跃假设。我们设计了一个逻辑，可以原因的客户端使用这些操作的终止，而不会打破他们的抽象边界，和操作的实现相对于他们的抽象规范的正确性。我们引入了一个新的语义模型，使用分层的主观义务来表达活性不变量，和一个证明系统，这是健全的模型。我们的规范和推理的微妙之处说明了使用几个案例研究。
2021-11-30 cs.LO cs.PL
Resource Analysis driven by (Conditional) Termination Proofs
当程序具有复杂的控制流时，现有的资源分析技术产生成本关系系统（CRS），其成本函数保留程序的复杂流，因此可能无法求解为封闭形式的上界。本文提出了一种新的方法，资源分析，是由终止分析的结果驱动。其基本思想是，终止证明封装的流程的程序，这是相关的成本计算，以便，通过驱动的CRS使用终止证明的生成，我们产生一个线性有界的CRS（LB-CRS）。一个LB-CRS是由成本函数，保证是局部有界的线性排序函数，从而大大简化了CRS的解决过程。我们已经构建了一个新的资源分析工具，名为MaxCore，它由VeryMax终止分析器指导，并使用CoFloCo和PUBS作为CRS求解器。我们对2019年C语言程序复杂性和终止性竞赛的基准测试的实验结果表明，MaxCore优于所有其他资源分析工具。正在考虑接受TPLP。
2019-07-23 cs.LO cs.PL
On the Termination Problem for Probabilistic Higher-Order Recursive Programs
The University of Tokyo（东京大学）；University of Bologna（博洛尼亚大学）；Aix Marseille Univ, Université de Toulon, CNRS, LIS（艾克斯-马赛大学，土伦大学，法国国家科学研究中心，信息系统实验室）
本文针对概率高阶模型检查问题展开研究，引入PHORS作为概率高阶程序模型，证明二阶PHORS几乎必然终止性不可判定，给出终止概率不动点刻画并实现了近似计算过程，经初步实验验证其运行良好。
2026-08-20 cs.LO cs.PL
Termination Analysis of Probabilistic Programs through Positivstellensatz's
我们考虑不确定性概率程序的最基本的活性性质的终止。我们提出了有效的方法，终止分析的非确定性概率程序与多项式后卫和转让。我们的方法是通过合成的多项式排名上鞅，这一方面显着推广线性排名上鞅，另一方面是一个对应的多项式排名功能证明终止的非概率程序。该方法通过Positivstellenales的综合多项式秩上鞅，产生一个有效的方法，这不仅是声音，但也是半完全的一个大子类的程序。我们的实验结果表明，我们的方法可以处理几个经典的程序与复杂的多项式后卫和分配，并可以合成有效的二次排序上鞅时，线性不存在，即使是简单的仿射规划。
2016-04-25 cs.PL
Termination of canonical context-sensitive rewriting and productivity of rewrite systems
程序的终止，即，不存在无限的计算，确保了所有初始表达式的范式的存在，从而为函数式程序的规范化语义的定义提供了必要的成分。然而，在惰性函数式语言中，无限的数据结构通常作为计算的结果来交付。例如，所有素数的列表可以作为数值表达式或数据结构的永不结束的流返回。如果允许这样的流，要求终止是无望的。在这种情况下，生产力的概念可以用来提供一个无限数据结构计算的帐户，因为它“捕捉了可计算性的概念，无限列表程序的进展”（B.A. Sijtsma，On the Productivity of Recursive List Definitions，ACM Transactions on程序设计语言and Systems 11（4）：633-649，1989）。然而，在领域的长期重写系统，这可以被看作是（一阶，无类型，无条件）的功能程序，上下文敏感重写（CSR）的终止已被证明相当于重写系统的生产力，通过适当的转换。通过这种方式，可以使用证明CSR终止的工具来证明生产力。在术语重写中，CSR是当仅允许对函数符号的选定参数进行约简时产生的重写限制。在本文中，我们表明，众所周知的CSR的计算能力的结果是有用的，以更好地了解现有的重写系统的生产力和终止CSR之间的联系，并获得更强大的技术来证明重写系统的生产力。
2015-12-22 cs.LO cs.PL
A Devil's Advocate against Termination of Direct Recursion
魔鬼的拥护者是一个反对一个主张的人，不是作为一个坚定的对手，而是为了确定这个主张的有效性。我们感兴趣的是一个反对终止程序的魔鬼代言人。他通过产生一个可以导致原始程序不终止的恶意程序来做到这一点。通过检查和运行恶意程序，可以深入了解不终止的潜在原因，并产生终止的反例。我们介绍我们的方法使用并发程序设计语言约束处理规则（约束）。与其他声明性语言一样，非终止性通过无限递归发生。给定一个自递归规则，我们自动地从它生成一个或多个魔鬼规则。魔鬼规则的构造很简单，不需要猜测。魔鬼的规则很简单。例如，对于具有单递归的规则，它们是非递归的。我们表明，魔鬼的规则是最大的邪恶在以下意义上：对于任何程序，包含自递归规则和任何无限计算，通过该规则在该程序中，有一个相应的无限计算与递归规则和魔鬼的规则。在这种情况下，恶意规则充当非终止性的有限见证。另一方面，如果魔鬼规则不表现出无限的计算，递归规则是无条件终止的。我们还确定的情况下，静态分析的魔鬼的规则决定终止或不终止的递归规则。
2017-01-10 cs.LO cs.PL cs.SE
Automated Termination Analysis of Polynomial Probabilistic Programs
概率程序的终止行为取决于随机分配的结果。几乎确定终止（AST）是关于程序是否在所有可能的输入上以概率1终止的问题。正几乎必然终止（Positive Almost Sure Termination，PAST）是指在有限的期望步数内终止。本文提出了一种完全自动化的方法来终止分析的概率时程序，其后卫和表达式是多项式表达式。由于证明（正）AST一般是不可判定的，现有的证明规则通常提供了充分的条件。这些条件大多涉及上鞅的约束。我们认为，从文献中的四个证明规则，并扩展这些与现有的证明规则的概括（P）AST。我们自动化的证明规则，有效地计算渐近界多项式的程序变量。这些界限被用来决定一个证明规则的充分条件-包括上鞅的约束条件。因此，我们的软件工具琥珀可以检查AST，PAST，以及他们的否定的一个大类的多项式概率程序，同时进行终止推理完全与多项式证人。实验结果表明，我们的广义证明规则的优点，并证明琥珀可以处理概率程序，是其他国家的最先进的工具。
2021-01-28 cs.PL
Modular termination verification with a higher-order concurrent separation logic (Intermediate report)
我们报告的中间结果，我们的研究推理活性属性，除了深正确性的一个命令，并发程序设计语言与高阶存储。目前，我们集中在一个特定的活性属性，即终止。通过保证终止性，我们可以将部分正确性的陈述加强为完全正确性。这是通过将终止性转换为安全属性的经典方法来实现的。特别是，我们扩展的程序设计语言考虑与调用权限，这已被证明，使模块化的推理终止。添加原子块是为了增加我们基于调用权限的方法的表现力。我们的工作建立在Iris --一个基础的、机器检查的、高阶并发分离逻辑框架--之上，而不修改它。有了这些补充，我们就能够模块化地推理并发但非阻塞算法的终止。我们对正在考虑的程序设计语言的添加保留了Iris对帮助和预言进行推理的能力。作为一个例子，我们将当前的系统应用于现有的无锁并发堆栈的案例研究，并在Iris中得到了证明。最后，我们概述了扩展阻塞并发方法的后续步骤。
2022-12-28 cs.LO cs.PL
Termination of Nondeterministic Recursive Probabilistic Programs
研究了非确定性递归概率规划的终止问题。首先，我们证明了基于秩上鞅的方法对于有界终结（即，所有调度器上的有界预期终止时间）。我们的结果也澄清了以前的结果，声称排名上鞅是不是一个完整的方法，即使是不确定的概率程序没有递归。其次，我们证明了条件差有界的排序上鞅提供了一个合理的方法，期望终止时间的下界。最后，我们证明了条件绝对差下界的上鞅为几乎肯定终止提供了一个合理的方法，以及在给定的步骤数内的非终止尾概率的明确界限。我们还提出了几个启发性的反例，建立一定的先决条件（如条件差分有界条件）的必要性。
2017-01-11 cs.PL
Neural Termination Analysis
University of Birmingham（伯明翰大学）；Amazon, Inc.（亚马逊公司）；University of Oxford（牛津大学）
我们介绍了一种新的方法来自动终止分析的计算机程序：我们使用神经网络来表示排名功能。排名函数将程序状态映射到从下到上有界的值，并随着程序的运行而减少;排名函数的存在证明程序终止。我们训练一个神经网络从采样的执行轨迹的程序，使网络的输出沿轨迹减少，然后，我们使用符号推理正式验证，它概括到所有可能的执行。在肯定的答案，我们获得一个正式的证书终止程序，我们称之为神经排名功能。我们证明，由于神经网络的能力，代表非线性函数，我们的方法成功的程序，是超出了国家的最先进的工具。这包括在循环条件中使用析取的程序和包含非线性表达式的程序。
2022-09-06 cs.LG cs.LO cs.PL
A General Framework for Automatic Termination Analysis of Logic Programs
本文描述了一个逻辑程序自动终止分析的一般框架，其中我们用“终止”来理解为程序和给定查询构造的LD树的有限性。证明了无限LD-树的分支的某个子集到有限集的映射的一个一般性质。从这一结果导出几个终止定理，通过使用不同的有限集。前两个是制定谓词依赖和原子依赖图。然后证明了与程序相关的查询-映射对的一般结果（参见图1）。\cite{Sagiv,Lindenstrauss:Sagiv}）。在\cite{Lindenstrauss:Sagiv:Serebrenik}中描述的{ \em TermiLog}系统的正确性由此而来。在这个系统中，不可能证明涉及算术谓词的程序的终止性，因为整数的通常顺序不是有根据的。本文提出了一种新的方法，它可以很容易地结合在{ \em TermiLog}或类似的系统中，这使得它有可能证明终止程序涉及算术谓词。它是基于一个有限的整数抽象与查询映射对的技术相结合，基本上是能够划分为几种情况下，这样一个简单的终止功能足以为每种情况下的终止证明。最后概述了几种可能的扩展。
2000-12-13 cs.PL
Inference of termination conditions for numerical loops
本文提出了一种新的分析逻辑程序中数值计算终止性的方法。传统的方法由于整数的非良基性而无法对其进行分析。我们提出了一种技术，可以克服这些困难。我们的方法是基于转换程序的方式，允许集成和扩展技术最初开发的数值计算分析的框架中的查询映射对与知名的框架的可接受性。这样的整合不仅有助于理解终止行为的数值计算，但也允许自动执行正确的分析，这样的计算，从而扩展以前的工作基于约束的方法终止。在本文的最后一节中，我们讨论了可能的扩展技术，包括将一般的长期订单。
2001-06-26 cs.LO cs.PL
Termination analysis of logic programs using acceptability with general term orders
提出了一种新的逻辑程序终止性分析方法。该方法的本质是，我们利用一般的术语排序（而不是级别映射），就像在逻辑程序终止分析的转换方法中所做的那样，但是我们将这些排序直接应用于逻辑程序，而不是通过一些转换获得的术语重写系统。我们定义了一些变量的可接受性，一般术语排序的基础上，并显示它们是如何等同于LD-终止。我们开发了一个需求驱动的，基于约束的方法来验证这些可接受的变量。该方法优于标准可接受性的优点是，在某些情况下，需要复杂的级别映射，可以很容易地生成相当简单的术语排序。与转换方法相比，它的优点是完全避免了转换步骤。
2000-11-17 cs.PL
Probabilistic Termination by Monadic Affine Sized Typing (Long Version)
我们引入了一个系统的一元仿射大小的类型，这基本上概括了通常的大小类型，并允许这种方式来捕捉概率高阶程序几乎肯定终止。超越普通的、强规范化而不失去可靠性是一项艰巨的任务，如果没有更丰富的、定量的类型概念，而且没有施加一些亲和性约束，这是无法完成的。建议的类型系统是强大的，足以类型的经典例子的概率终止程序，如随机游走。类型化程序被证明几乎必然终止的方法是基于归约的，但需要对该技术进行实质性的修改。
2017-01-15 cs.LO cs.PL
Formalizing Termination Proofs under Polynomial Quasi-interpretations
函数式程序的终止性证明需要检查所有可能的归约路径。由于这种约简树的高度和大小之间的指数差距，没有朴素的形式化终止证明产生给定程序的多项式复杂度的连接。我们利用极小函数图的概念解决了这个问题，极小函数图是一个项及其范式的一组对，它被定义为单调算子的最小不动点。我们表明，终止证明的程序减少字典路径顺序（LPOs为短）和多项式准可解释的，可以最佳地进行在一个弱片段的Peano算法。这产生了另一种证明，即由LPO终止的多项式准可解释程序计算的每个函数在多项式空间中是可计算的。形式化确实是最优的，因为每个多项式空间可计算函数都可以由这样的程序计算。关键的观察是，在LPO终止程序下的最小函数图的归纳定义可以近似于沿着LPO的超限归纳。
2015-09-10 cs.CC cs.LO cs.PL
Proving False in Object-Oriented Verification Programs by Exploiting Non-Termination
我们研究了三种不同的面向对象程序验证器：Gobra、KeY和Dafny。我们表明，所有这三个可以证明假使用一个简单的技巧与幽灵变量声明和非终止代码。这表明，这些语言的验证器可以产生不合理的结果，没有太大的困难，这可能是所有面向对象的验证器共同的。
2022-12-05 cs.PL
On Lexicographic Proof Rules for Probabilistic Termination
我们认为几乎肯定（A. S.）概率程序的终止问题，它是经典命令式程序的随机扩展。字典序排序函数为非概率程序的终止提供了一种合理而实用的方法，并通过字典序排序上鞅（LexRSMs）将其扩展到概率程序.然而，在以前的工作中引入的LexRSM有一个限制，这阻碍了它们的自动化：它们的所有组件必须在所有可达状态中是非负的。这可能导致LexRSM不存在，即使是简单的终止程序。我们的贡献是双重的：首先，我们引入了一个广义的LexRSM允许某些组件是负的。非概率终止证明的这个标准特征迄今为止在概率环境中还不知道是合理的，因为合理性证明需要仔细分析潜在的随机过程。其次，我们提出了多项式时间算法，使用我们的广义LexRSM证明a.s.终止在广泛的线性算术程序类。
2021-08-04 cs.PL
Automatic Termination Analysis of Programs Containing Arithmetic Predicates
对于带有算术谓词的逻辑程序，显示终止并不容易，因为整数的通常顺序并没有充分的根据。一种新的方法，很容易纳入TermiLog系统的自动终止分析，在这种情况下，显示终止。该方法包括以下步骤：首先，自动推导出表示整数值域的有限抽象域。在此基础上，对程序进行抽象解释.其结果是一个有限数量的原子抽象的答案查询，用于扩展查询映射对的技术。对于每个潜在非终止的查询映射对，猜测有界（整数值）终止函数。如果遍历该对减少了终止函数的值，则建立终止。简单的函数通常足以满足每个查询映射对，这使我们的方法比传统方法更有优势，传统方法对所有循环使用单个终止函数，这必然会更复杂，更难自动猜测。值得注意的是，McCarthy的91函数的终止可以使用我们的方法自动显示。总之，所提出的方法是基于结合的查询映射对的技术的整数的有限抽象，并且基本上是能够划分为几种情况下，这样一个简单的终止功能足以为每种情况下的终止证明。因此，证明终止的整个过程可以在TermiLog和类似系统的框架内自动完成。
2000-11-23 cs.PL
Inference of termination conditions for numerical loops in Prolog
本文提出了一种新的分析逻辑程序中数值计算终止性的方法。传统的方法由于整数的非良基性而无法对其进行分析。我们提出了一种技术，可以克服这些困难。我们的方法是基于转换程序的方式，允许集成和扩展技术最初开发的数值计算分析的框架中的查询映射对与知名的框架的可接受性。这样的整合不仅有助于理解终止行为的数值计算，而且还允许我们自动执行正确的分析，这样的计算，通过扩展以前的工作基于约束的方法终止。最后，我们讨论了可能的扩展的技术，包括将一般术语排序。
2003-07-10 cs.LO cs.PL
A Non-Termination Criterion for Binary Constraint Logic Programs
一方面，逻辑程序的终止性分析现在是逻辑编程社区中一个相当成熟的研究课题。另一方面，非终止性分析似乎仍然是一个不太吸引人的主题。如果把这条研究路线分为动态分析和静态分析两种方法，本文属于后者。它提出了一个标准，检测非终止原子查询的二进制CLP规则，严格概括了我们以前的工作在这个问题上。我们给出了一个通用的操作定义和实现的逻辑形式，这个标准。然后，我们证明了逻辑形式是正确的和完整的操作定义。
2009-01-10 cs.PL
DynamiTe: Dynamic Termination and Non-termination Proofs
有越来越多的兴趣在终止推理的非线性规划，同时，最近的动态策略表明，他们能够推断出不变量，这样的挑战性的计划。这些进展使我们假设，也许这种非线性不变量的动态策略可以适用于学习递归集（非终止）和/或排名功能（终止）。在本文中，我们利用动态分析，并提请终止和非终止以及静态和动态策略更紧密地结合在一起，以处理非线性规划。对于终止，我们的算法从具体的传递闭包中推断出排名函数，对于非终止，该算法迭代地收集执行并动态学习条件以改进递归集。最后，我们描述了一个集成的算法，允许这些算法相互通知对方，采取反例从一个努力失败的验证和交叉的静态/动态和终止/非终止线，以创建新的执行样本的其他。
2020-10-12 cs.PL
An Improved Non-Termination Criterion for Binary Constraint Logic Programs
一方面，逻辑程序的终止性分析现在是逻辑编程社区中一个相当成熟的研究课题。另一方面，非终止性分析似乎仍然是一个不太吸引人的主题。如果把这条研究路线分为动态分析和静态分析两种方法，本文属于后者。它提出了一个标准，检测非终止原子查询的二进制CLP条款，严格概括了我们以前的工作在这个问题上。我们给出了这一准则的一般操作定义和逻辑形式。然后，我们证明了逻辑形式是正确的和完整的操作定义。
2005-08-24 cs.PL
cTI: A constraint-based termination inference tool for ISO-Prolog
我们提出了cTI，第一个系统的通用左终止推理的逻辑程序。终止性推理推广了终止性分析和检验。传统上，终止分析器试图证明给定类的查询终止。这个类必须提供给系统，例如通过用户注释的方式。此外，每次更新感兴趣的查询类时，都必须重新进行分析。相反，终止推理既不需要用户注释，也不需要重新计算。在这种方法中，立即推断所有谓词的终止类。我们描述了CTI的体系结构，并报告了一个广泛的实验评估系统，包括许多经典的例子，从逻辑编程终止文学和几个Prolog程序的体面的大小和复杂性。
2003-09-16 cs.PL
Ghost Signals: Verifying Termination of Busy-Waiting (Extended Version)
多处理器机器的程序通常执行忙等待同步。我们提出了第一个分离逻辑模块化验证终止的公平调度下，这样的程序。我们的逻辑要求证明作者将虚信号与每个忙等待循环相关联，并允许这样的循环在其相应的信号$s$未设置时停止。证明作者还必须对信号定义有根据的顺序，并证明如果循环线程持有设置信号$s^\prime$的义务，则$s^\prime$的顺序高于$s$。通过使用传统的共享状态不变量将重影信号的状态与数据结构的状态相关联，可以验证在任意数据结构上忙等待任意条件的程序。
2021-05-18 cs.LO cs.PL
On Termination of Polynomial Programs with Equality Conditions
研究了一类多路多项式规划的终止问题，其中对程序变量的所有赋值都是多项式，循环和条件语句的测试条件都是多项式等式.我们表明，这样的程序的非终止输入（NTI）的集合是算法可计算的，从而导致其终止的可判定性。据我们所知，所考虑的MPP家族是迄今为止可决定终止的最大家族。本文给出了一个显式的递归函数，它本质上是阿克曼的，用来计算多项式理想在控制函数下的升链的最大长度，从而得到了Seidenberg问题的完整答案.这个最大的长度有利于我们的算法计算NTI和决定终止MPP的精确的复杂性分析。我们扩展我们的方法与多项式守护命令的程序，并显示如何不完整的程序与不等式警卫的MPP可以得到。我们的技术的多项式程序的不变生成的应用。
2020-09-01 cs.PL cs.SC
Proving Almost-Sure Termination of Probabilistic Programs via Incremental Pruning
经典的命令式程序的实值随机变量和随机分支的扩展产生了概率程序。终止问题是此类程序最基本的活性性质之一。定性（也称为几乎肯定）终止问题询问给定程序是否以概率1终止。排序函数为非概率规划的终止提供了一种完善的方法，而将其推广到概率规划则是通过排序上鞅（Ranking Supermartingales，RSM）实现的。RSM已经扩展到字典式RSM，以处理涉及控制流结构的程序，以及组合方法。现有的基于RSM的方法有两个主要的局限性：首先，字典式的基于RSM的方法需要一个强的非负性假设，这并不总是需要满足。现有的基于RSM的算法方法的第二个关键限制是它们依赖于预先计算的不变量。依赖于预先计算的不变量的主要缺点是不一致性和低效率的权衡：弱不变量可能不足以让RSM证明终止，而使用强不变量会导致计算效率低下。我们的贡献是双重的：首先，我们展示了如何放松强非负性条件，并仍然提供可靠性保证几乎肯定终止。其次，我们提出了一个增量的方法，计算字典的RSM的过程中进行迭代修剪的程序，已经被证明是终止的部分，与安全证明。特别是，我们的技术不依赖于强大的预先计算的不变量。我们目前的实验结果表明，我们的方法的适用性，从文献中的概率程序的例子。
2021-08-06 cs.PL
Stochastic Invariants for Probabilistic Termination
终止性是活性的基本性质之一，本文研究了实变量概率规划的终止性问题。以前的工作集中在定性问题，问是否输入程序终止概率~1（几乎肯定终止）。一个强有力的方法，这个定性问题的概念排名上鞅关于一组给定的不变量。定量问题（概率终止）要求终止概率的界限。现有的方法来解决概率终止的一个基本的和概念上的缺点是，即使上鞅考虑的概率行为的程序，获得的不变量完全忽略了概率方面。在这项工作中，我们解决的概率终止问题的线性算术概率程序的非确定性。我们定义了{ \em随机不变量}的概念，这是约束以及约束保持的概率界。引入了{ \em排斥上鞅}的概念。首先，我们证明了排斥上鞅可以用来获得随机不变量的概率上界。其次，我们从以下三个方面证明了排斥上鞅的有效性：（1）结合秩上鞅和排斥上鞅，我们可以计算终止概率的下界;（2）排斥上鞅为反驳几乎必然终止提供了证据;（3）结合秩上鞅和排斥上鞅，我们可以建立概率规划的持久性.我们还提出了相关的计算问题的结果和实验评估我们的方法在学术上的例子。
2016-11-16 cs.PL
Why Can't You Behave? Non-termination Analysis of Direct Recursive Rules with Constraints
本文关注的是基于规则的程序出错。规则应用程序的不良行为是计算不终止或失败。我们提出了一个静态的程序分析的非终止性问题的递归约束处理规则（约束处理规则）的语言。是一种涉及约束推理的高级并发声明语言。它与许多其他基于规则的方法密切相关，因此其结果具有更广泛的意义。在这样的语言中，非终止性是由于递归规则的无限应用。失败是由于在计算过程中矛盾约束的积累。我们给出了线性直接递归简化规则的潜在非终止性和失效（以及确定终止性）的具有所谓的不良行为条件的定理。递归规则中约束之间的逻辑关系在这种程序分析中起着至关重要的作用。我们认为，我们的方法可以扩展到其他类型的递归和更一般的一类规则。因此，本文可以作为一个基本的参考和进一步研究的起点。
2017-01-10 cs.LO cs.PL cs.SE
Acceptability with general orderings
提出了一种新的逻辑程序终止性分析方法。该方法的本质是我们使用一般的排序（而不是级别映射），就像在逻辑程序终止分析的转换方法中所做的那样，但是我们将这些排序直接应用于逻辑程序，而不是通过一些转换获得的术语重写系统。我们定义了一些变量的可接受性，一般的排序的基础上，并显示它们是如何等同于LD-终止。我们开发了一个需求驱动的，基于约束的方法来验证这些可接受的变量。该方法优于标准可接受性的优点是，在某些情况下，需要复杂的级别映射，可以很容易地生成相当简单的排序。与转换方法相比，它的优点是完全避免了转换步骤。{ \bf Keywords：}终止分析、可接受性、排序。
2001-06-26 cs.LO cs.PL
Automatic HFL(Z) Validity Checking for Program Verification
本文提出了一种自动化的方法来检验HFL（Z）公式的有效性，HFL（Z）是一种高阶逻辑，具有不动点算子和整数。结合Kobayashi et al.的减少，从高阶程序验证HFL（Z）的有效性检查，我们的方法产生一个全自动的，统一的验证方法的任意时间属性的高阶功能程序表示的模态μ演算，包括终止，非终止，公平终止，公平非终止，也分支时间属性。我们已经实现了我们的方法，并取得了可喜的实验结果。
2022-12-09 cs.PL
Type-Based Termination for Futures
本文将顺序语言中的大小类型终止性检查方法适配到并发场景，通过扩展半公理化相继式演算提出大小类型细化方案，借助无限宽有限深的类型推导树和新颖逻辑关系论证，实现基于futures的函数式并发程序的终止性验证。
2024-04-15 cs.LO cs.PL
Proving Non-termination by Program Reversal
提出了一种新的证明非确定整数规划非终止性的方法。我们的技术相当简单但有效。它依赖于一个纯粹的语法反转的程序的过渡系统，其次是一个基于约束的不变的合成与约束来自原始和反转的过渡系统。后一项任务是通过简单调用现成的SMT求解器来执行的，这使我们能够利用SMT求解的最新进展。此外，我们的方法提供了一个组合的功能不存在（作为一个整体）在以前的方法：它处理程序的非确定性，提供相对完整性的保证，并支持程序与多项式算术。与我们的原型工具RevTerm进行的实验表明，我们的方法，尽管它的简单性和更强的理论保证，是至少与国家的最先进的工具，往往实现了一个不平凡的改进下，其参数的适当配置。
2021-04-02 cs.PL
Synthesis of models for order-sorted first-order theories using linear algebra and constraint solving
声明性程序终止分析的最新发展强调使用适当的模型作为一种通用的方法来证明声明性程序的终止性的逻辑理论代表的程序处于危险之中。在这种情况下，顺序排序的一阶逻辑提供了一个强大的框架来表示声明性程序。它还提供了一个目标逻辑，以通过转换获得其他逻辑的模型。我们研究了顺序排序的一阶逻辑的数值模型的自动生成及其在程序分析中的应用，特别是在声明式程序的终止分析中。我们使用凸域给域的不同种类的顺序排序的签名，我们解释排序的签名通过适当适应凸矩阵的解释排名的符号。这种数值解释允许使用现有的算法和工具，从线性代数和算术约束求解合成的模型。
2015-12-22 cs.LO cs.PL
