Linear Ranking for Linear Lasso Programs
这项工作的一般设置是基于约束的合成终止参数。我们考虑一类受限制的程序，称为套索程序。lasso程序的终止参数是一对排名函数和不变量。我们提出-据我们所知-第一种方法来合成终止参数套索程序，使用线性算术。我们证明了一个完备性定理。完备性定理表明，即使我们只使用线性（而不是非线性）约束求解，我们也能够在几种有趣的情况下计算终止参数。我们的方法的关键在于一个约束转换，用一个和来代替一个析取。
2014-01-21 cs.LO
Ranking Function Synthesis for Linear Lasso Programs
这项工作的范围是限制类的程序称为线性套索程序的终止参数的约束为基础的合成。一个终止参数由一个排序函数和一组支持不变量组成。我们以几种方式扩展现有的方法。首先，我们使用Motzkin的转置定理代替Farkas引理。这使我们可以考虑线性套索规划，可以额外包含严格的不等式。现有的方法仅限于非严格不等式和等式。其次，我们考虑几种排序函数：仿射线性，分段和字典排序函数。此外，我们提出了一种新的排序函数，称为多相排序函数，它通过固定数量的相位进行，使得对于每个相位，有一个仿射线性排序函数。作为一个抽象的具体排名功能的合成，我们介绍了排名功能模板的概念。这使我们能够以统一的方式处理所有排名功能。我们的方法依赖于非线性代数约束求解作为一个子程序，这是众所周知的规模差，大的问题。作为缓解，我们正式评估我们的约束的难度，并提出一个论点，为什么他们是一个更容易的一种比一般的非线性约束。我们证明我们的方法是完整的：如果有一个终止参数的形式指定的给定的排名功能模板与固定数量的仿射线性支持不变量，那么我们的方法将找到一个终止参数。据我们所知，我们提出的方法是最强大的技术，基于合成的发现终止参数的线性套索程序，并包含和增强了几种方法已经提出到目前为止。
2014-01-21 cs.LO
Ranking Functions for Vector Addition Systems
向量加法系统是理论计算机科学中的一个重要模型，已被广泛用于系统分析。终止性是向量加法系统的一个重要性质，在文献中引起了广泛的兴趣。本文给出了一种构造状态向量加法系统秩函数的完整方法。对排序函数的兴趣是由这样一个事实激发的，即排序函数在终止的情况下提供了有价值的额外信息：它们提供了对矢量加法系统的进展的解释，可以向验证工具的用户报告，并且可以用作终止的证书。此外，我们展示了如何排名功能可以用于矢量加法系统的计算复杂性分析（这里的复杂性是指的步骤数的矢量加法系统分析可以采取在给定的初始向量）。
2017-10-23 cs.LO
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
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
Complexity Bounds for Ordinal-Based Termination
“如果我们在一个给定的形式系统中证明了一个定理，那么除了它的真实性之外，我们还知道什么呢？我们在程序终止证明的特定背景下研究Kreisel的问题，着眼于推导程序运行时间的复杂性界限。我们的主要工具，这是长度函数定理，它提供了复杂性的界限上使用良好的准秩序。我们说明了如何证明这样的定理在简单的情况下，但到目前为止未经处理的序数。我们将展示如何应用这一新的定理来推导程序的复杂性界限时，他们被证明终止感谢到一些序数的排名功能。
2014-07-22 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
Synthesising Interprocedural Bit-Precise Termination Proofs (extended version)
证明程序终止是保证没有不良行为的关键，例如挂起程序，甚至是拒绝服务攻击等安全漏洞。为了使终止检查规模的大型系统，跨过程终止分析似乎是必不可少的，这是一个在很大程度上未开发的研究领域，在终止分析，其中大部分精力都集中在困难的单过程问题。我们提出了一个模块化终止分析C程序使用基于模板的过程间总结。我们的分析结合了上下文敏感的，过度近似的前向分析与推断下近似终止的前提条件。位精确的终止参数是在字典式线性排名函数模板上合成的。我们的实验结果表明，我们的工具2LS优于国家的最先进的替代品，并证明了明显的优势，过程间推理整体分析的效率，同时保持相当的精度。
2015-05-18 cs.LO cs.SE
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
2LS: Heap Analysis and Memory Safety (Competition Contribution)
2LS是一个分析顺序C程序的框架，可以验证和反驳程序断言和终止。2LS框架建立在CPROVER基础设施之上，并实现了基于模板的合成技术，例如找到不变量和排名函数，以及增量循环展开技术来找到反例和k-归纳证明。今年版本的主要改进是2LS分析程序的能力，这些程序需要对动态数据结构的形状和内容进行组合推理，以及用于存储器安全属性的仪器。
2020-01-03 cs.LO cs.SE
Any-k Algorithms for Enumerating Ranked Answers to Conjunctive Queries
提出any-k算法，通过下推排序到连接中，实现合取查询排序答案的高效枚举，复杂度为O(n+klogk)，优于传统先连接后排序方法。
2023-10-12 cs.DB cs.DS cs.LO
