Termination Analysis of Programs with Multiphase Control-Flow
具有多阶段控制流的程序是执行通过几个（可能是隐式的）阶段的程序。证明这些程序的终止（或推断相应的运行时边界）通常具有挑战性，因为它需要分别对这些阶段进行推理。本文讨论了证明这类程序可终止性的技术，特别是：（1）使用多阶段排序函数，其中我们将讨论几种程序表示的排序函数的理论问题;以及（2）使用控制流细化，特别是约束Horn子句的部分评估，以简化控制流，除其他外，用更简单的排序函数证明终止性。
2021-09-10 cs.LO cs.PL
Termination Analysis for the $π$-Calculus by Reduction to Sequential Program Termination
我们提出了一个自动化的方法来证明终止的$π$演算过程，减少终止顺序程序的基础上：我们翻译一个$π$演算过程的顺序程序，使后者的终止意味着前者。然后，我们可以使用现成的终止验证工具来检查顺序程序的终止。我们的方法部分受到了邓和Sangiorgi对$π$演算的终止分析的启发，并通过将这样的通信链转换为目标顺序程序中的递归函数调用链，来检查复制输入通道上是否存在无限的通信链。我们已经实现了一个自动化的工具，所提出的方法的基础上，并确认其有效性。
2021-09-01 cs.PL
Non-Termination Proving: 100 Million LoC and Beyond
Bloomberg, New York, USA（花旗集团纽约总部）；Imperial College London, UK（伦敦帝国理工学院）；Meta FAIR, London, UK（Meta FAIR伦敦总部）；University College London, UK（伦敦大学学院）
针对现有非终止性检测工具难以适配大规模真实代码的问题，研究团队推出组合式下近似的证明工具Pulse Infinite，在超1亿行多语言代码中检出30余个新问题，刷新该领域技术水平。
2025-09-05 cs.CL cs.PL cs.SE
Almost-Sure Termination by Guarded Refinement
本文提出Caliper，一种基于受保护递归和概率耦合的高阶分离逻辑，通过证明程序与简单模型间的精化来建立概率程序的几乎必然终止，并在Coq中验证多个示例。
2024-11-11 cs.LO cs.PL
On Modular Termination Proofs of General Logic Programs
该研究提出一种基于可接受程序概念的模块化方法，可通过单独处理层级模块证明含否定的通用逻辑程序终止性，针对良模式、良类型程序给出验证技术与迭代证明法，能大幅简化证明。
2001-07-30 cs.LO cs.PL
On termination of meta-programs
术语{ \em元编程}指的是编写将其他程序作为数据并利用其语义的程序的能力。本文的目的是提出一种方法，使我们能够执行一个正确的终止分析广泛的实用元解释器，包括否定和执行不同的任务在执行过程中。它是基于结合的权力，一般秩序，用于证明终止的长期重写系统和程序，并在著名的可接受性条件，用于证明终止的逻辑程序。该方法建立证明解释程序的终止所需的排序与证明元解释器连同该解释程序的终止所需的排序之间的关系。如果建立了这种关系，其中一个关系的终止意味着另一个关系的终止，即，元解释器保留终止。在元解释器中，正确分析的是构造元解释器的证明树，不同类型的跟踪器和推理器。不带附录出现在逻辑程序设计理论与实践中。
2003-12-24 cs.LO cs.PL
Well-definedness of Streams by Transformation and Termination
流是给定数据类型上的无限序列。流规范是用于定义流的一组等式。我们提出了一个转换，从这样的流规范的一个长期重写系统（TRS），在这样的方式，所得到的TRS的终止意味着流规范是定义良好的，也就是说，承认一个独特的解决方案。因此，证明良好的定义的几个有趣的流规范可以完全自动地使用目前强大的工具来证明TRS终止。为了增加这种方法的力量，我们研究了保持语义和良好定义的转换。我们给出了一些示例，其中上述技术适用于转换后的规范，而对于原始规范则失败。
2010-09-07 cs.LO cs.PL
A Calculus for Modular Loop Acceleration and Non-Termination Proofs
循环加速可以用来证明程序的安全性、可达性、运行时界限和（非）终止性。为此，已经提出了各种加速技术。然而，到目前为止，所有这些都是单一的，即，不能使用几种不同加速技术的组合来加速单个循环。相比之下，我们提出了一个演算，允许以模块化的方式结合加速技术，我们展示了如何将许多现有的加速技术集成到我们的演算。此外，我们提出了两种新的加速技术，可以无缝地纳入我们的微积分。其中一些加速技术仅适用于非终止循环。因此，将它们与我们的新演算相结合，产生了一种新的模块化方法来证明非终止性。实证评估表明，我们的方法的适用性，无论是循环加速和证明不终止。
2022-06-08 cs.LO cs.PL
Termination Analysis of Probabilistic Programs through Positivstellensatz's
我们考虑不确定性概率程序的最基本的活性性质的终止。我们提出了有效的方法，终止分析的非确定性概率程序与多项式后卫和转让。我们的方法是通过合成的多项式排名上鞅，这一方面显着推广线性排名上鞅，另一方面是一个对应的多项式排名功能证明终止的非概率程序。该方法通过Positivstellenales的综合多项式秩上鞅，产生一个有效的方法，这不仅是声音，但也是半完全的一个大子类的程序。我们的实验结果表明，我们的方法可以处理几个经典的程序与复杂的多项式后卫和分配，并可以合成有效的二次排序上鞅时，线性不存在，即使是简单的仿射规划。
2016-04-25 cs.PL
A static higher-order dependency pair framework
我们重新审视了证明高阶项重写终止性的静态依赖对方法，并在许多方面对其进行了扩展：（1）我们引入了一种新的重写形式主义，设计用于高阶重写的终止性证明，具有元变量的代数泛函系统。(2)我们提供了一个语法检查的合理性标准，使该方法适用于一个大类的重写系统。(3)我们提出了一个模块化的依赖对框架，这种高阶设置。(4)我们引入了一个细粒度的概念，形成和可计算的链，使框架更强大。(5)我们制定了几个现有的和新的终止证明技术在我们的框架内的处理器的形式。该框架已在（全自动）高阶终止工具WANDA中实现。
2019-04-04 cs.LO cs.PL
Non-Termination Analysis of Java Bytecode
本文介绍了一种全自动的静态分析，它以一个顺序Java字节码程序P为输入，试图证明P的无限执行。该技术包括将P编译成一个约束逻辑程序P_CLP，并证明P_CLP的非终止性;当P由被精确编译成约束的指令组成时，我们的方法可以处理方法调用;据我们所知，它是第一个静态的Java字节码方法，能够证明存在无限递归。我们已经在Julia分析器中实现了我们的技术。我们已经比较了Julia在一组113个程序上的结果与AProVE和Invel提供的结果，AProVE和Invel是我们所知道的唯一可与我们相比的免费使用的非终止分析器。只有Julia可以检测到无限递归的非终止性。
2014-01-21 cs.PL
On Lexicographic Proof Rules for Probabilistic Termination
我们认为几乎肯定（A. S.）概率程序的终止问题，它是经典命令式程序的随机扩展。字典序排序函数为非概率程序的终止提供了一种合理而实用的方法，并通过字典序排序上鞅（LexRSMs）将其扩展到概率程序.然而，在以前的工作中引入的LexRSM有一个限制，这阻碍了它们的自动化：它们的所有组件必须在所有可达状态中是非负的。这可能导致LexRSM不存在，即使是简单的终止程序。我们的贡献是双重的：首先，我们引入了一个广义的LexRSM允许某些组件是负的。非概率终止证明的这个标准特征迄今为止在概率环境中还不知道是合理的，因为合理性证明需要仔细分析潜在的随机过程。其次，我们提出了多项式时间算法，使用我们的广义LexRSM证明a.s.终止在广泛的线性算术程序类。
2021-08-04 cs.PL
Automated Termination Analysis for Logic Programs with Cut
可终止性是逻辑程序的一个重要性质，也是研究得很好的性质。然而，几乎所有的自动终止分析方法都集中在确定的逻辑程序上，而实际的Prolog程序通常使用cut运算符。本文介绍了一种新的预处理方法，它能自动地将Prolog程序转换成无割的逻辑程序，其中无割程序的终止意味着原程序的终止。因此，在该预处理之后，可以应用用于证明确定逻辑程序的终止的任何技术。我们在我们的终止证明程序AProVE中实现了这种预处理，并成功地进行了广泛的实验。
2010-07-28 cs.LO cs.PL
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report
多处理器机器的程序通常执行忙等待同步。在本文中，我们向证明终止这类程序的第一步。我们近似（i）任意等待事件的突然程序终止和（ii）忙碌等待事件的忙碌等待被突然终止。我们提出了一个分离逻辑模块化验证终止（公平调度下）的程序，其中一些线程最终突然终止程序，和其他线程忙等待这种情况发生。
2020-07-21 cs.LO cs.PL
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit
多处理器机器的程序通常执行忙等待同步。在本文中，我们向证明终止这类程序的第一步。我们近似（i）任意等待事件的突然程序终止和（ii）忙碌等待事件的忙碌等待被突然终止。我们提出了一个分离逻辑模块化验证终止（公平调度下）的程序，其中一些线程最终突然终止程序，和其他线程忙等待这种情况发生。
2020-10-16 cs.LO cs.PL
Proving Correctness and Completeness of Normal Programs - a Declarative Approach
我们提倡使用声明性方法来证明逻辑程序的属性。完全正确性可以分为正确性、完整性和干净终止;后者包括非挣扎。只有干净的终止依赖于操作语义，特别是选择规则。我们展示了如何处理的正确性和完整性的声明方式，治疗程序只从逻辑的角度来看。这种方法中使用的规范是解释（或理论）。我们指出，规范的正确性可能不同于那些完整性，因为通常有答案，既不被认为是错误的，也不需要计算。给出了确定性程序正确性和完备性的证明方法，并将其推广到正规程序。对于正常的程序，我们使用3值完成语义;这是一个标准的语义对应于否定有限失败。证明方法仅采用经典的2值逻辑。我们使用的3值完成语义，这可能是单独的利益的2值表征。所提出的方法进行了比较与基于操作语义的方法。我们还采用这项工作的想法推广一个已知的方法证明终止正常程序。
2005-01-25 cs.LO cs.PL
Automated Termination Analysis of Polynomial Probabilistic Programs
概率程序的终止行为取决于随机分配的结果。几乎确定终止（AST）是关于程序是否在所有可能的输入上以概率1终止的问题。正几乎必然终止（Positive Almost Sure Termination，PAST）是指在有限的期望步数内终止。本文提出了一种完全自动化的方法来终止分析的概率时程序，其后卫和表达式是多项式表达式。由于证明（正）AST一般是不可判定的，现有的证明规则通常提供了充分的条件。这些条件大多涉及上鞅的约束。我们认为，从文献中的四个证明规则，并扩展这些与现有的证明规则的概括（P）AST。我们自动化的证明规则，有效地计算渐近界多项式的程序变量。这些界限被用来决定一个证明规则的充分条件-包括上鞅的约束条件。因此，我们的软件工具琥珀可以检查AST，PAST，以及他们的否定的一个大类的多项式概率程序，同时进行终止推理完全与多项式证人。实验结果表明，我们的广义证明规则的优点，并证明琥珀可以处理概率程序，是其他国家的最先进的工具。
2021-01-28 cs.PL
Automatic Termination Analysis of Programs Containing Arithmetic Predicates
对于带有算术谓词的逻辑程序，显示终止并不容易，因为整数的通常顺序并没有充分的根据。一种新的方法，很容易纳入TermiLog系统的自动终止分析，在这种情况下，显示终止。该方法包括以下步骤：首先，自动推导出表示整数值域的有限抽象域。在此基础上，对程序进行抽象解释.其结果是一个有限数量的原子抽象的答案查询，用于扩展查询映射对的技术。对于每个潜在非终止的查询映射对，猜测有界（整数值）终止函数。如果遍历该对减少了终止函数的值，则建立终止。简单的函数通常足以满足每个查询映射对，这使我们的方法比传统方法更有优势，传统方法对所有循环使用单个终止函数，这必然会更复杂，更难自动猜测。值得注意的是，McCarthy的91函数的终止可以使用我们的方法自动显示。总之，所提出的方法是基于结合的查询映射对的技术的整数的有限抽象，并且基本上是能够划分为几种情况下，这样一个简单的终止功能足以为每种情况下的终止证明。因此，证明终止的整个过程可以在TermiLog和类似系统的框架内自动完成。
2000-11-23 cs.PL
Eventual Linear Ranking Functions
程序终止性是程序分析中的一个研究热点。在过去的几年里，已经见证了用于程序设计语言（如C和Java）的终止分析器的发展，其具有显著的精度和性能。这些系统在很大程度上是基于来自声明式约束编程领域的技术和工具。在本文中，我们首先回顾了一个算法的基础上法卡斯引理发现线性排名功能证明终止的某一类循环。然后，我们提出了一个扩展的方法来显示存在的最终线性排名功能，即，线性函数，在循环的有限展开之后成为排名函数。证明了算法的正确性和完备性。
2013-06-08 cs.PL
While Loops in Coq
本文提出在 Coq 浅层嵌入的命令式语言中引入 while 循环的方法，通过一种可定义可能不终止递归函数的通用技术解决 Coq 对终止证明的要求，并以链表程序验证其有效性。
2023-09-25 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
Supermartingales, Ranking Functions and Probabilistic Lambda Calculus
在连续随机抽样和显式递归的λ演算中，基于排序上鞅，给出了几乎必然终止的一种证明方法。这一结果在三个方面得到了推广。反音排名函数对它们必须下降的速度限制较弱，并且适用于更广泛的程序。稀疏排名函数只在程序可达状态的子集上取值，因此定义起来更简单，也更灵活。排名功能方面的替代减少战略提供了更大的灵活性，并显着增加了适用性的排名上鞅的方法来证明几乎肯定的终止，由于一个新的（限制）合流的结果，这是独立的利益。反调排序函数的概念受到McIver、Morgan、Kaminski和Katoen在一阶命令式语言中的类似工作的启发，但适用于高阶函数式语言。稀疏排名功能和合流语义扩展是唯一的高阶设置。我们的方法可以用来证明几乎肯定终止的程序，是超出了文献中的方法，包括高阶和非仿射递归。
2021-04-30 cs.LO 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
Automated Theorem Proving for Prolog Verification
université de La Réunion（留尼汪大学）
本文提出通过将LPTP的公理转换为一阶公式并利用自动定理证明器验证Prolog程序属性。
2026-01-07 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
Proving LTL Properties of Bitvector Programs and Decompiled Binaries (Extended)
人们越来越感兴趣的是将验证工具应用于具有位向量操作的程序（例如，二进制文件）。SMT求解器作为这些工具的基础，因此通过位爆破和线性算术近似增加了对位向量推理的支持。在本文中，我们表明，类似的线性算术近似位向量操作可以在源代码级别通过转换。具体来说，我们引入了新的路径，这些路径通过线性条件/约束过度近似位向量操作，增加了分支，但使我们能够更好地利用成熟的整数推理和验证工具的插值。我们发现，对于位向量程序的可达性，增加分支会产生微不足道的开销，但与整数插值优化相结合时，使更多的程序进行验证。我们进一步表明，这种利用整数插值在常见的情况下，也使竞争终止验证的位向量程序，并导致第一个有效的技术LTL验证的位向量程序。最后，我们提供了一个深入的案例研究反编译（“提升”）二进制程序，模拟X86执行通过频繁使用的位向量操作。我们提出了一个新的工具DarkSea，第一个工具能够验证可达性，终止和LTL的解除二进制文件。
2021-08-28 cs.FL cs.PL cs.SE
A New Proof Rule for Almost-Sure Termination
概率程序的一个重要问题是它所有发散运行的概率质量是否为零，也就是说它“几乎必然”终止。证明这一点可能很难，本文提出了一种新的方法来做到这一点;它是在程序逻辑中表达的，因此直接适用于源代码。程序可能包含概率选择和恶魔选择，概率选择可能取决于当前状态。和其他研究人员一样，我们使用变量函数（也称为变量函数）。“超鞅”）是实值的，并且在每次循环迭代中概率可能会减少;但我们的关键创新在于减少的数量和概率是参数的。我们证明了新的规则的合理性，表明其适用性超出现有的规则，并解释其连接到经典的结果可数（非恶魔）马尔可夫链。
2017-12-26 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
Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs
本文提出了一个wp风格的演算获得的概率程序的期望运行时间的界限。它的应用包括确定（可能无限）的期望终止时间的概率程序和证明积极的几乎必然终止-一个程序终止概率1在有限的期望时间？我们提供了几个证明规则的运行时间的循环，并证明了一个简单的操作模型的方法的可靠性。我们表明，我们的方法是一个保守的扩展Nielson的方法推理确定性程序的运行时。我们分析了一些示例程序的预期运行时间，包括一维随机游走和优惠券收集器问题。
2017-11-28 cs.LO cs.PL
Non-polynomial Worst-Case Analysis of Recursive Programs
我们研究开发有效方法来证明非确定性递归程序最坏情况界限的问题。秩函数是证明非递归程序的终止性和最坏情况界的可靠而完备的方法。首先，我们将排序函数应用于递归，从而得到度量函数。我们表明，测量功能提供了一个健全的和完整的方法来证明最坏情况下的非确定性递归程序的界限。我们的第二个贡献是合成的非多项式形式的测量功能。我们表明，非多项式的测量函数的对数和指数可以通过抽象的对数或指数项，法卡斯引理，和Handelman定理使用线性规划合成。虽然以前的方法获得最坏情况下的多项式边界，我们的方法可以合成的形式$\mathcal{O}(n\log n)$以及$\mathcal{O}(n^r)$，其中$r$不是一个整数的边界。我们提出的实验结果表明，我们的方法可以有效地获得经典的递归算法，如（i）合并排序，分治算法的最接近对问题，在这里我们获得$\mathcal{O}(n \log n)$最坏情况下的界限，和（ii）Karatsuba的算法多项式乘法和Strassen的算法矩阵乘法的最坏情况下的界限，其中我们获得$\mathcal{O}(n^r)$界限，使得$r$不是整数并且接近于各个算法的最佳已知界限。
2017-04-30 cs.PL
