Distilling Programs to Prove Termination
确定任何程序是否终止的问题被图灵证明是不可判定的，但该领域的最新进展已经允许为一大类程序确定此信息。决定程序是否终止的经典方法可以追溯到图灵本人，涉及到找到一个将程序状态映射到良序的排序函数，然后证明这个函数的结果对于每个可能的程序转换都是递减的。最近证明终止性的方法涉及从搜索单个排名函数转向搜索一组排名函数;这组是排名函数的选择，并使用了析取终止参数。在本文中，我们描述了一种新的技术，用于确定程序是否终止。我们的技术被应用到蒸馏程序转换的输出，将程序转换成一个简化的形式称为蒸馏形式。在蒸馏形式的程序被转换成相应的标记的过渡系统和终止可以证明，通过这个标记的过渡系统的所有可能的无限的痕迹将导致一个无限的下降，有根据的数据值。我们证明了我们的技术上的一些例子，并将其与以前的工作。
2020-08-07 cs.LO
Termination Analysis of Programs with Multiphase Control-Flow
具有多阶段控制流的程序是执行通过几个（可能是隐式的）阶段的程序。证明这些程序的终止（或推断相应的运行时边界）通常具有挑战性，因为它需要分别对这些阶段进行推理。本文讨论了证明这类程序可终止性的技术，特别是：（1）使用多阶段排序函数，其中我们将讨论几种程序表示的排序函数的理论问题;以及（2）使用控制流细化，特别是约束Horn子句的部分评估，以简化控制流，除其他外，用更简单的排序函数证明终止性。
2021-09-10 cs.LO cs.PL
Decision Tree Learning in CEGIS-Based Termination Analysis
提出了一种新的基于决策树的排序函数综合算法，用于验证程序的可终止性.我们的算法集成到反例引导归纳合成（CEGIS）的工作流程。CEGIS是一个迭代学习模型，在每次迭代中，（1）合成器从当前示例中合成候选解决方案，（2）验证器接受候选解决方案，如果它是正确的，或者拒绝它，提供反例作为下一个示例的一部分。我们的主要创新之处是在合成器的设计：建立在一个通常的决策树学习算法，我们的算法检测周期的一组例子过渡，并使用它们来细化决策树。我们已经实现了所提出的方法，并取得了可喜的实验结果，现有的基准集（非）终止验证问题，需要合成分段定义的字典仿射排名功能。
2021-07-05 cs.LO
Neural Termination Analysis
University of Birmingham（伯明翰大学）；Amazon, Inc.（亚马逊公司）；University of Oxford（牛津大学）
我们介绍了一种新的方法来自动终止分析的计算机程序：我们使用神经网络来表示排名功能。排名函数将程序状态映射到从下到上有界的值，并随着程序的运行而减少;排名函数的存在证明程序终止。我们训练一个神经网络从采样的执行轨迹的程序，使网络的输出沿轨迹减少，然后，我们使用符号推理正式验证，它概括到所有可能的执行。在肯定的答案，我们获得一个正式的证书终止程序，我们称之为神经排名功能。我们证明，由于神经网络的能力，代表非线性函数，我们的方法成功的程序，是超出了国家的最先进的工具。这包括在循环条件中使用析取的程序和包含非线性表达式的程序。
2022-09-06 cs.LG cs.LO cs.PL
Termination of $λ$$Π$ modulo rewriting using the size-change principle (work in progress)
大小变化终止原理最初被用来研究一阶函数程序的终止问题。在这项工作中，我们表明，它也可以用来研究终止高阶重写系统中的依赖类型扩展LF。
2018-12-05 cs.LO
Supermartingales, Ranking Functions and Probabilistic Lambda Calculus
在连续随机抽样和显式递归的λ演算中，基于排序上鞅，给出了几乎必然终止的一种证明方法。这一结果在三个方面得到了推广。反音排名函数对它们必须下降的速度限制较弱，并且适用于更广泛的程序。稀疏排名函数只在程序可达状态的子集上取值，因此定义起来更简单，也更灵活。排名功能方面的替代减少战略提供了更大的灵活性，并显着增加了适用性的排名上鞅的方法来证明几乎肯定的终止，由于一个新的（限制）合流的结果，这是独立的利益。反调排序函数的概念受到McIver、Morgan、Kaminski和Katoen在一阶命令式语言中的类似工作的启发，但适用于高阶函数式语言。稀疏排名功能和合流语义扩展是唯一的高阶设置。我们的方法可以用来证明几乎肯定终止的程序，是超出了文献中的方法，包括高阶和非仿射递归。
2021-04-30 cs.LO cs.PL
The Automatic Synthesis of Linear Ranking Functions: The Complete Unabridged Version
证明通用顺序计算机程序终止的经典技术涉及程序的每个循环的排序函数的合成。线性排名函数特别有趣，因为许多终止循环都允许线性排名函数，并且存在自动合成线性排名函数的算法。本文提出了两种这样的算法：一种基于Sohn和Van Gelder 1991年的工作;另一种是Podelski和Rybalchenko于2004年提出的。值得注意的是，虽然这两种算法将在完全相同的条件下合成一个线性排序函数，但前者大多是未知的终止分析社区，其普遍适用性在本文之前从未提出过。在本文中，我们彻底证明这两种算法，我们证明了他们的正确性，我们比较他们的最坏情况下的复杂性和实验评估其效率，我们提出了一个开源的实现，他们将很容易包括终止分析功能的自动程序验证。
2012-04-01 cs.LO cs.PL
Ranking Templates for Linear Loops
提出了一种基于线性排序模板的线性循环程序终止参数约束综合的新方法。线性排序模板是参数化的、有良好基础的关系，使得对参数的分配产生排序函数。这种方法概括了现有的方法，使我们能够使用模板的许多不同的排名功能与仿射线性组件。我们讨论模板多相，分段，字典排序功能。由于这些排序模板需要严格和非严格的不等式，我们使用Motzkin的换位定理，而不是法卡斯引理转换生成的$\exists\forall$ -约束到一个$\exists$ -约束。
2014-01-21 cs.LO
A theory of function-induced-orders to study recursion termination
函数的终止性是可计算性理论中的一个重要问题。在本文中，我们证明了一个函数的重复迭代可以诱导其域集合的元素之间的顺序。由此得到的偏序集的哈塞图看起来像一个森林，有一个可能的基集和一个生成集（在论文中定义）。同构森林可能会出现不同的功能和等价类，因此，形成。在此基础上，研究了一类确定性终止函数，证明了存在一个自排序程序，它可以证明自己的终止性，以及一个泛终止函数，从它可以导出所有其它的终止函数.
2017-08-15 cs.LO
Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings
Tel Aviv University（特拉维夫大学）；Certora；Weizmann Institute of Science（魏茨曼科学研究所）
通过计时器和排名验证无限状态系统的首阶时间属性，利用隐式排名和SMT求解器实现终止性证明。
2026-01-19 cs.LO cs.PL
Ranking Templates for Linear Loops
提出了一种基于线性排序模板的线性循环程序终止参数约束综合的新方法。线性排序模板是参数化的、有良好基础的关系，使得对参数的分配产生排序函数。我们的方法概括了现有的方法，使我们能够使用模板的许多不同的排名功能与仿射线性组件。我们讨论模板多相，嵌套，分段，并行和字典排序功能。这些排名模板可以组合成更强大的模板。由于这些排序模板需要严格和非严格的不等式，我们使用Motzkin的换位定理，而不是法卡斯引理转换生成的$\exists\forall$ -约束到一个$\exists$ -约束。
2015-03-29 cs.LO
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
Complexity Bounds for Ordinal-Based Termination
“如果我们在一个给定的形式系统中证明了一个定理，那么除了它的真实性之外，我们还知道什么呢？我们在程序终止证明的特定背景下研究Kreisel的问题，着眼于推导程序运行时间的复杂性界限。我们的主要工具，这是长度函数定理，它提供了复杂性的界限上使用良好的准秩序。我们说明了如何证明这样的定理在简单的情况下，但到目前为止未经处理的序数。我们将展示如何应用这一新的定理来推导程序的复杂性界限时，他们被证明终止感谢到一些序数的排名功能。
2014-07-22 cs.LO
Synthesising Interprocedural Bit-Precise Termination Proofs (extended version)
证明程序终止是保证没有不良行为的关键，例如挂起程序，甚至是拒绝服务攻击等安全漏洞。为了使终止检查规模的大型系统，跨过程终止分析似乎是必不可少的，这是一个在很大程度上未开发的研究领域，在终止分析，其中大部分精力都集中在困难的单过程问题。我们提出了一个模块化终止分析C程序使用基于模板的过程间总结。我们的分析结合了上下文敏感的，过度近似的前向分析与推断下近似终止的前提条件。位精确的终止参数是在字典式线性排名函数模板上合成的。我们的实验结果表明，我们的工具2LS优于国家的最先进的替代品，并证明了明显的优势，过程间推理整体分析的效率，同时保持相当的精度。
2015-05-18 cs.LO cs.SE
Monotonicity Constraints for Termination in the Integer Domain
大小变化终止（SCT）是一种基于无限下降不可能性的程序终止性证明方法。为此，我们使用一个程序抽象，其中过渡描述的单调性约束（抽象）变量。当只允许形式为x>y'和x \geq y'的约束时，我们有大小变化图。在过去的十年中，理论和实践都在这个有限的框架内发生了重大变化。过去大多数工作的关键基本假设是变量的域是有根据的。在最近的一篇论文中，我展示了如何将一些理论从大小变化图的域扩展到一般的单调性约束，从而补充了以前的工作，但仍然停留在良基域的领域。然而，单调性约束，有趣的是，能够证明终止也在整数域中，这是没有根据的。本文的目的是探讨单调性约束在这一领域中的应用。我们奠定了必要的理论基础，并提出了精确的决策程序终止;最后，我们提供了一个程序来构建明确的全球排名功能的单调性约束在单指数时间，最佳的最坏情况下的大小和尺寸（序数）。
2011-08-22 cs.LO
The Size-Change Termination Principle for Constructor Based Languages
本文描述了一个通用的ML风格的一阶按值调用语言的自动终止检查器。我们利用值是从变量和元组构建的这一事实来保留一些关于递归调用的参数在计算期间如何演变的信息。其结果是一个标准的终止扩展的大小变化终止原则的李，琼斯和本-阿姆拉姆，可以检测大小变化内的子值的参数。此外，相应的算法是易于实现，使其成为一个很好的候选人的实验。
2014-02-12 cs.LO cs.PL
Ranking Functions for Linear-Constraint Loops
本文研究整数变量线性约束循环中线性及字典序线性排序函数的存在性问题，证明一般情形为 coNP 完全，识别 PTIME 特例并给出完整综合算法。
2025-09-29 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
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
Breaking the Mold: Nonlinear Ranking Function Synthesis Without Templates
本文研究非线性多项式秩函数合成问题，通过在整数/实数环理论中工作绕过不可判定性障碍，提出了一种无需模板的完备终止分析方法，适用于无界维度和次数的字典序秩函数。
2024-09-26 cs.LO cs.PL
On Multiphase-Linear Ranking Functions
多阶段排序函数（$\mathit{MΦRFs}$）被提出作为证明循环终止的手段，在该循环中，计算通过多个“阶段”进行，并且每个阶段的进展由不同的线性排序函数描述。我们的工作提供了新的见解，这些功能的线性约束（单路径循环）的结合所描述的循环。我们提供了一个完整的多项式时间的解决方案的问题的存在性和合成的$\mathit{MΦRF}$的有界深度（相位数），当变量范围超过合理或实数;一个完整的解决方案（更难）的情况下，变量是整数，与匹配的下限证明，表明这个问题是CONP-完全的;和一个新的定理，它限制了循环的迭代次数与$\mathit{MΦRFs}$。令人惊讶的是，即使所涉及的变量以非线性方式变化，边界也是线性的。我们还考虑了一种类型的字典排序功能，$\mathit{LLRFs}$，更有表现力的字典功能的完整的解决方案，迄今为止。我们证明，对于上述类型的循环，字典功能可以减少到$\mathit{MΦRFs}$，从而检测和合成的复杂性的问题，以及由此产生的迭代范围，也回答了这个类。
2017-03-23 cs.LO cs.PL
The Hardness of Finding Linear Ranking Functions for Lasso Programs
确定线性约束循环是否具有线性排序函数是理解循环行为、证明其终止性和建立迭代边界的重要关键。如果没有提供前提条件，则已知当变量范围在整数上时决策问题在coNP中，而对于有理数或实数，决策问题在PTIME中。在这里，我们表明，决定是否一个线性约束循环的前提条件，特别是部分指定的输入，有一个线性排名功能是EXPSPACE硬的整数，和PSPACE硬的有理数。这些决策问题的精确复杂性尚不清楚。EXPSPACE下界是从Petri网的可达性问题（等价于向量加法系统）中推导出来的，并且可能表示一个更强的下界（受制于VAS理论中的开放问题）。有理数的下界来自于布尔程序的一种新的模拟。下界也给出了问题的决定，如果一个线性排名功能支持一个特定形式的归纳不变存在。对于整数上的循环，问题对于凸多面体不变量是PSPACE-困难的，对于下闭自然数集作为不变量是EXPSPACE-困难的。
2014-08-26 cs.CC cs.LO
Bounded Termination of Monotonicity-Constraint Transition Systems
直觉上，如果我们能证明一个程序终止，我们期望得到一些关于它的复杂性的结论。但是，从终止证明到复杂性界限的过程并不总是清楚的。在这项工作中，我们考虑单调性约束过渡系统，一个程序抽象的终止是可判定的（基于大小变化终止原则）。我们表明，这些程序也有一个可判定的复杂性属性：可以确定是否所有的过渡序列的长度可以有界的初始状态。这就是有界终止问题。有趣的是，如果存在一个界限，它必须是多项式的。我们证明了有界终止问题是PSPACE-完全的。我们还讨论了，理论上，使用的抽象程序上的界限来推断一个具体的程序，已被抽象的结论。结论可能是一个多项式时间界，或在其他情况下多项式空间或指数时间。我们认为，单调性约束抽象的承诺是有用的程序的实际复杂性分析。
2014-04-30 cs.FL cs.LO
The Size-Change Principle for Mixed Inductive and Coinductive types
本文针对嵌套归纳与余归纳类型，改进大小变化原理以检查递归定义的完全性，确保其相对于相应类型的正确性。
2025-09-02 cs.LO
2LS: Heap Analysis and Memory Safety (Competition Contribution)
2LS是一个分析顺序C程序的框架，可以验证和反驳程序断言和终止。2LS框架建立在CPROVER基础设施之上，并实现了基于模板的合成技术，例如找到不变量和排名函数，以及增量循环展开技术来找到反例和k-归纳证明。今年版本的主要改进是2LS分析程序的能力，这些程序需要对动态数据结构的形状和内容进行组合推理，以及用于存储器安全属性的仪器。
2020-01-03 cs.LO cs.SE
