Proving Looping and Non-Looping Non-Termination by Finite Automata
提出了一种新的证明项重写非终止性的方法。其基本思想是找到一个非空的项的正则语言，它在重写下是封闭的，并且不包含范式。它是自动化的，用一个有固定数量状态的树自动机来表示语言，并用SAT公式来表达上述要求。这个公式的可满足性意味着不终止。我们的方法成功的许多例子，所有早期的技术失败，例如从组合逻辑的S规则。
2015-05-03 cs.LO
Proving Non-Termination by Acceleration Driven Clause Learning
本文将加速驱动子句学习（ADCL）适配到迁移系统，提出 ADCL-NT 变体用于证明程序非终止性，并在 LoAT 工具中实现和评估。
2023-07-07 cs.LO
Proving Termination of Normalization Functions for Conditional Expressions
Boyer和Moore讨论了一个递归函数，它将条件表达式转换为范式[1]。很难证明这个函数在所有输入端都终止。比较了三种终止性证明：（1）使用测度函数，（2）在Domain理论中使用LCF，（3）证明了由递归调用模式定义的递归关系是有根据的。最后两个证明本质上是相同的，但在明显不同的逻辑框架进行。这两个证明的“计算意义”是正规化函数的一个明显的全变式。相关函数进行嵌套递归调用。三个终止性证明变得更加复杂：终止性和正确性必须同时证明。递归关系的方法似乎足够灵活，以处理微妙的终止证明，以前域理论似乎是必不可少的。
2000-10-02 cs.LO
Sparse Tiling through Overlap Closures for Termination of String Rewriting
我们在字符串重写中过度近似可达集，这是由可接受因子（称为瓦片）定义的语言。一个稀疏的瓦片集只包含那些在派生中可到达的瓦片，并且通过完成自动机来构造。利用语义标记的稀疏分片定义的部分代数，我们得到了一个证明局部终止性的变换方法。利用前向闭包的已知结果和重叠闭包的新特征，我们分别获得了证明终止性和相对终止性的方法。我们报告显示这些方法的强度的实验。
2020-03-03 cs.LO
Non-termination using Regular Languages
我们描述了一种方法来证明非循环不终止，即长期重写系统不承认循环减少。作为非终止证书，我们采用常规（树）自动机。
2014-05-22 cs.LO
Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs
证明程序终止通常通过为程序状态找到有充分根据的排名函数来完成。现有的终止证明器通常使用线性代数或模板来找到排名函数。因此，他们经常被限制在寻找数学整数上的线性排名函数。这类函数不足以证明许多终止程序的终止性，此外，对于数学整数操作的程序的终止参数并不总是导致对于固定宽度机器整数操作的同一程序的终止参数。我们提出了一个终止分析能够产生非线性，字典排序功能和非线性递归集是正确的固定宽度的机器算术和浮点运算我们的技术是基于减少从程序\emph{termination}二阶\emph{satisfaction}。我们提供了配方的终止和非终止在一个片段的二阶逻辑有限域上可判定的限制量化。由此产生的技术是一个健全的和完整的分析有限状态程序的终止固定宽度的整数和IEEE浮点运算。
2014-10-19 cs.LO
Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting
本文提出首个用于概率项重写系统最内层重写的依赖对框架，以分析期望复杂度并证明强几乎必然终止，并在AProVE中实现，展示了其优势。
2025-10-15 cs.LO
Termination of Cycle Rewriting by Transformation and Matrix Interpretation
我们提出的技术，以证明终止循环重写，即字符串重写的周期，这是字符串的开始和结束连接。我们的主要技术是将循环重写转换为字符串重写，然后应用最先进的技术来证明字符串重写系统的终止性。我们提出了三个这样的转换，并证明他们都是健全的和完整的。这样，不仅变换系统的串重写的终止意味着原始循环重写系统的终止，对于非终止也可以得出类似的结论。除了这种转换的方法，我们提出了一个统一的框架矩阵的解释，涵盖了大多数早期的方法来自动证明终止循环重写。我们所有的技术都用于证明终止和相对终止。我们提出了几个实验显示我们的技术的力量。
2017-03-16 cs.LO
A Unified Ordering for Termination Proving
我们引入了一个约简顺序称为加权路径顺序（WPO），它包含了许多现有的约简顺序。WPO比较Knuth-Beneficiary order（KBO）中的项权重，而WPO允许通过广泛的解释来计算权重。我们调查总结，多项式和最大值这样的解释。我们表明，KBO是一个限制的情况下，WPO引起的求和，多项式的顺序（POLO）是由WPO引起的多项式，和字典路径顺序（LPO）是一个限制的情况下，WPO引起的极大值。通过结合这些解释，我们得到了一个WPO的例子，统一KBO，LPO和POLO。为了适应现代依赖对框架中的WPO，我们进一步提供了基于WPO和部分状态的约简对。作为约简对，WPO也包含矩阵解释。最后，我们提出了我们的技术的SMT编码，并通过实验证明我们的工作的意义。
2014-04-24 cs.LO
Proving Termination of Graph Transformation Systems using Weighted Type Graphs over Semirings
本文提出基于有序半环的加权类型图方法，将矩阵解释推广到图重写，通过权重递减证明图变换系统的均匀终止性，并在工具Grez中实现。
2023-10-11 cs.FL cs.LO
Proving termination with transition invariants of height omega
Podelski和Rybalchenko的终止定理指出，从任何初始状态终止的归约关系正是其传递闭包（仅限于可达状态）包含在某些良基关系的有限并中的归约关系。该定理的另一种陈述是，终止约化关系正是那些具有“反言有理的转变不变量”的关系。根据这个结果，同一作者和Byron Cook设计了一个算法来检查while-if程序终止的充分条件。该算法寻找一个析取的良好基础的过渡不变量，由良好基础的关系的高度Ω，如果它找到它，它推导出终止的while-if程序使用终止定理。这就提出了一个有趣的问题：当每个关系都有高度Ω时，具有析取良基转换不变量的归约关系的状态是什么？这个问题的答案可以导致一组while-if程序的终止算法可以证明是终止的表征。本文的目的是证明它们是高度为ω ^n的约化关系的集合，其中n <ω。此外，如果转移不变量中的所有关系都是本原递归的，且归约关系是本原递归映射对某个本原递归集的限制的图，则最终状态可由初始状态下的某个本原递归映射计算.作为一个推论，我们得出的一组功能，有至少一个实现Podelski Rybalchenko while-if语言与一个良好的基础析取过渡不变，其中每个关系的高度Ω，正是一组原始递归函数。
2014-07-17 cs.LO
Proving Termination of Unfolding Graph Rewriting for General Safe Recursion
本文给出了一种新的展开图重写的终止性证明和复杂性分析，展开图重写是一种特殊的无限图重写，它表达了安全递归的一般形式。我们引入了一个终止顺序的条款序列连同长期图的解释成序列的条款。展开图重写规则表示一般的安全递归可以成功地嵌入到终止顺序的解释，产生多项式的运行时复杂度。此外，推广的展开图重写规则的定义一般安全递归，我们提出了一个新的标准的多项式运行时复杂性的无限GRS和多项式大小的范式在无限GRS。
2014-06-20 cs.CC cs.LO math.LO
Proving termination of evaluation for System F with control operators
我们提出了新的证明，终止评估约简语义（即，具有显式表示求值上下文的小步操作语义）。我们介绍了一个修改版本的吉拉德的证明方法的基础上reductioncandidates，reductionpredicates定义的值和评价上下文所规定的减少语义格式。我们解决这两个流产的控制操作符（callcc）和定界控制操作符（移位和复位），我们引入新的多态类型系统，我们认为调用的值和调用的名称评估策略。
2013-09-05 cs.LO cs.PL
Termination of Graph Transformation Systems via Generalized Weighted Type Graphs
Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）
本文提出了一种改进的加权类型图方法，用于证明图变换系统的终止性，并将其推广到其他范畴。
2026-02-26 cs.LO
Local Termination: theory and practice
终止使用良好的基础单调代数的表征是自动终止技术的一个里程碑，在过去的几年里，我们已经看到了广泛的发展。术语重写系统（TRS）的语义特征和大多数已知的终止方法都涉及全局终止，即所有术语的一致终止。在本文中，我们考虑本地终止，在一个给定的TRS的特定条款集。本文的主要目标是概括的语义特征的整体终止本地终止。这是可能的，通过承认良基单调代数是部分的。我们还将我们的方法扩展到本地相对终止。对局部终止的兴趣自然出现在程序验证中，在那里人们可能只对合理的输入感兴趣，或者只是想验证程序终止的输入集。当处理TRS中已知为非终止的特定类别的术语时，局部终止也将是感兴趣的，例如组合逻辑（CL）或TRS编码递归程序方案或图灵机。我们展示了如何证明全球终止的一些著名的技术，如逐步删除重写规则和语义标签，可以适应当地的情况。我们还描述了减少局部到全局终止问题的转换。由此产生的证明本地终止的技术在某些情况下已经自动化。我们的应用之一涉及CL作为正则语言的终止S-项的特征。在此之前，这种语言已经通过对S项的归约行为进行繁琐的分析而被发现。这些发现现在已经被一个完全自动化和经过验证的证明所证实。
2010-09-07 cs.LO
Monotonicity Constraints for Termination in the Integer Domain
大小变化终止（SCT）是一种基于无限下降不可能性的程序终止性证明方法。为此，我们使用一个程序抽象，其中过渡描述的单调性约束（抽象）变量。当只允许形式为x>y'和x \geq y'的约束时，我们有大小变化图。在过去的十年中，理论和实践都在这个有限的框架内发生了重大变化。过去大多数工作的关键基本假设是变量的域是有根据的。在最近的一篇论文中，我展示了如何将一些理论从大小变化图的域扩展到一般的单调性约束，从而补充了以前的工作，但仍然停留在良基域的领域。然而，单调性约束，有趣的是，能够证明终止也在整数域中，这是没有根据的。本文的目的是探讨单调性约束在这一领域中的应用。我们奠定了必要的理论基础，并提出了精确的决策程序终止;最后，我们提供了一个程序来构建明确的全球排名功能的单调性约束在单指数时间，最佳的最坏情况下的大小和尺寸（序数）。
2011-08-22 cs.LO
Termination Analysis of Programs with Multiphase Control-Flow
具有多阶段控制流的程序是执行通过几个（可能是隐式的）阶段的程序。证明这些程序的终止（或推断相应的运行时边界）通常具有挑战性，因为它需要分别对这些阶段进行推理。本文讨论了证明这类程序可终止性的技术，特别是：（1）使用多阶段排序函数，其中我们将讨论几种程序表示的排序函数的理论问题;以及（2）使用控制流细化，特别是约束Horn子句的部分评估，以简化控制流，除其他外，用更简单的排序函数证明终止性。
2021-09-10 cs.LO cs.PL
PaSTTeL: Parallel analysiS framework for Termination and non-Termination of Lasso programs
Sorbonne University, LIP6（索邦大学）；Paris-Nanterre University（巴黎楠泰尔大学）；Dowsers
提出PaSTTeL，一个模块化、通用的并行组合框架，统一了Lasso程序终止性分析的前沿方法，支持新算法集成、并发执行和嵌入外部项目，实验表现竞争力强。
2026-07-13 cs.LO
CeTA - A Tool for Certified Termination Analysis
自2004年第一次终止竞争以来，人们非常感兴趣的是，由终止工具自动生成的证明是否确实正确。终止证明技术的数量的增加以及生成的证明的复杂性的增加（例如，几种技术的组合、穷举标记、树自动机等），进行认证（即，检查这些证明的正确性对于人类来说越来越乏味。因此，人们对终止证明的自动认证感兴趣。这导致了使用证明助手（如Coq和Isabelle）进行认证的一般方法。我们目前的最新发展IsaFoR/CeTA（版本1.03），这是认证CeTA，基于Isabelle/HOL形式化重写IsaFoR。
2012-08-08 cs.LO
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
Termination Proofs for Logic Programs with Tabling
表格逻辑编程在逻辑编程社区中越来越受到关注。它避免了SLD执行的许多缺点，并为逻辑程序提供了一种更灵活且通常非常有效的执行机制。特别地，逻辑程序的表格执行比基于SLD解析的执行更频繁地终止。在这篇文章中，我们介绍了两个概念的通用终止逻辑编程与Tabling：准终止和（更强的概念）LG终止。我们提出了这两个概念的终止，即准可接受性和LG-可接受性的充分条件，我们表明，这些条件也是必要的情况下，制表是精心挑选的。从这些条件出发，我们给出了模终止证明，即，证明能够组合单独程序的终止证明以获得组合程序的终止证明。最后，在模式信息的存在下，我们陈述了充分条件，这些条件构成了以基于约束的方式自动证明终止的基础。
2000-03-09 cs.LO
Distilling Programs to Prove Termination
确定任何程序是否终止的问题被图灵证明是不可判定的，但该领域的最新进展已经允许为一大类程序确定此信息。决定程序是否终止的经典方法可以追溯到图灵本人，涉及到找到一个将程序状态映射到良序的排序函数，然后证明这个函数的结果对于每个可能的程序转换都是递减的。最近证明终止性的方法涉及从搜索单个排名函数转向搜索一组排名函数;这组是排名函数的选择，并使用了析取终止参数。在本文中，我们描述了一种新的技术，用于确定程序是否终止。我们的技术被应用到蒸馏程序转换的输出，将程序转换成一个简化的形式称为蒸馏形式。在蒸馏形式的程序被转换成相应的标记的过渡系统和终止可以证明，通过这个标记的过渡系统的所有可能的无限的痕迹将导致一个无限的下降，有根据的数据值。我们证明了我们的技术上的一些例子，并将其与以前的工作。
2020-08-07 cs.LO
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
A static higher-order dependency pair framework
我们重新审视了证明高阶项重写终止性的静态依赖对方法，并在许多方面对其进行了扩展：（1）我们引入了一种新的重写形式主义，设计用于高阶重写的终止性证明，具有元变量的代数泛函系统。(2)我们提供了一个语法检查的合理性标准，使该方法适用于一个大类的重写系统。(3)我们提出了一个模块化的依赖对框架，这种高阶设置。(4)我们引入了一个细粒度的概念，形成和可计算的链，使框架更强大。(5)我们制定了几个现有的和新的终止证明技术在我们的框架内的处理器的形式。该框架已在（全自动）高阶终止工具WANDA中实现。
2019-04-04 cs.LO cs.PL
Efficient Ranking Function-Based Termination Analysis with Bi-Directional Feedback
本文提出终止性分析框架Syndicate，通过双向反馈同时指导排序函数与循环不变量的搜索，在提升可证明终止程序数量的同时降低平均证明时间，性能优于现有工具。
2025-04-08 cs.LO
Polynomial Interpretations over the Natural, Rational and Real Numbers Revisited
多项式解释是证明项重写系统可终止性的一种有用技术。它们有各种各样的风格：多项式解释与真正的，合理的和整数系数。至于它们与终止性证明能力的关系，卢卡斯在2006年设法证明了存在重写系统，可以通过实（代数）系数的多项式解释来多项式终止，但不能仅使用有理系数的多项式来多项式终止。他还证明了相应的声明关于使用合理的系数与整数系数。在这篇文章中，我们扩展了这些结果，从而给出了多项式解释的上述变体之间的关系的全貌。特别是，我们表明，多项式的解释与真正的或合理的系数不subbranding多项式的解释与整数系数。我们的研究结果也适用于增量终止证明多项式的解释。
2014-09-16 cs.LO
Size-Change Termination, Monotonicity Constraints and Ranking Functions
大小变化终止（SCT）是一种基于无限下降不可能性的程序终止性证明方法。为此，我们可以使用一个程序抽象，其中的转换是由（抽象）变量上的单调性约束来描述的。当只允许形式为x>y'和x>=y'的约束时，我们有大小变化图。现在，理论和实践都在这个受限制的框架中比在单调性约束的一般框架中更有发展。本文表明，它是可能的，以延长和适应一些理论从域的大小变化图的一般情况下，从而补充以前的工作单调性约束。特别是，我们提出了精确的决策程序终止，我们提供了一个程序来构建明确的全球排名功能的单调性约束在单指数时间，这是更好的比迄今已公布的，即使是大小变化图。
2011-03-03 cs.LO
Automated Termination Analysis for Logic Programs with Cut
可终止性是逻辑程序的一个重要性质，也是研究得很好的性质。然而，几乎所有的自动终止分析方法都集中在确定的逻辑程序上，而实际的Prolog程序通常使用cut运算符。本文介绍了一种新的预处理方法，它能自动地将Prolog程序转换成无割的逻辑程序，其中无割程序的终止意味着原程序的终止。因此，在该预处理之后，可以应用用于证明确定逻辑程序的终止的任何技术。我们在我们的终止证明程序AProVE中实现了这种预处理，并成功地进行了广泛的实验。
2010-07-28 cs.LO cs.PL
Sound and Complete Proof Rules for Probabilistic Termination
本文针对结合离散概率选择和恶魔有界非确定性的命令式程序模型，提出了可靠且相对完备的定性与定量概率终止证明规则，利用超鞅和变体进行证明，并展示了其完备性及在二维随机游走中的应用。
2024-07-23 cs.LO
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
Synthesising Interprocedural Bit-Precise Termination Proofs (extended version)
证明程序终止是保证没有不良行为的关键，例如挂起程序，甚至是拒绝服务攻击等安全漏洞。为了使终止检查规模的大型系统，跨过程终止分析似乎是必不可少的，这是一个在很大程度上未开发的研究领域，在终止分析，其中大部分精力都集中在困难的单过程问题。我们提出了一个模块化终止分析C程序使用基于模板的过程间总结。我们的分析结合了上下文敏感的，过度近似的前向分析与推断下近似终止的前提条件。位精确的终止参数是在字典式线性排名函数模板上合成的。我们的实验结果表明，我们的工具2LS优于国家的最先进的替代品，并证明了明显的优势，过程间推理整体分析的效率，同时保持相当的精度。
2015-05-18 cs.LO cs.SE
Modular Termination for Second-Order Computation Rules and Application to Algebraic Effect Handlers
提出一种基于语义标注翻译和Blanqui一般模式的模块化终止性证明方法，实现为工具SOL，并成功应用于证明带代数效应处理器的调用-按-值演算变体的终止性。
2022-06-13 cs.LO cs.SC
Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction
霍尔逻辑的证明表是一个带有前置和后置条件的带注释程序，它对应于霍尔逻辑的一棵推理树。在本文中，我们证明了部分正确性的证明表可以转化为一个推理序列的重写归纳约束重写。我们还表明，如果从程序获得的约束重写系统正在终止，则所得序列是对应于霍尔三重组的归纳定理的有效证明。这样一个有效的证明与终止的约束重写系统意味着完全正确的程序w.r.t.霍尔三人组转换，使我们能够应用技术证明终止约束重写证明总正确性的程序连同证明表格的部分正确性。
2018-02-19 cs.LO
While Loops in Coq
本文提出在 Coq 浅层嵌入的命令式语言中引入 while 循环的方法，通过一种可定义可能不终止递归函数的通用技术解决 Coq 对终止证明的要求，并以链表程序验证其有效性。
2023-09-25 cs.LO cs.PL
A Higher-Order Logic for Concurrent Termination-Preserving Refinement
高阶并发语言的更精确的正确性证明是困难的：它们涉及到在并发的高级源语言和使用低级共享内存原语的实现之间建立一个保持终止的精化。然而，现有的逻辑证明并发加细要么忽略属性，如终止，或只处理一阶状态。在本文中，我们解决这些限制，扩展虹膜，最近的高阶并发分离逻辑，支持终止保留的细化推理。为了证明这些扩展的功能，我们证明了一个高阶，会话类型的语言的有效实现的正确性。据我们所知，这是第一个能够为这种语言提供编译器正确性证明的程序逻辑。我们的扩展和我们的编译器正确性证明的合理性已经在Coq中机械化。
2017-01-20 cs.LO cs.PL
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
概率程序验证的基本任务包括约束期望结果和证明有限期望运行时间内的终止性。我们贡献了一个简单而有效的归纳合成方法，证明这种定量的可达性属性生成归纳不变的源代码级。我们的实施显示了承诺：它为有限状态程序找到不变量，可以击败最先进的概率模型检查器，并且与致力于不变量合成和预期运行时推理的现代工具竞争。
2023-02-08 cs.LO
On Probabilistic Termination of Functional Programs with Continuous Distributions
本文研究了高阶概率函数程序的终止问题，包括递归、随机条件和连续分布抽样。关于具有连续分布的程序的终止概率的推理是困难的，因为终止执行的枚举不能提供任何非平凡的界限。我们提出了一个新的操作语义的基础上的痕迹的间隔，这是健全的和完整的标准采样为基础的语义，其中（可数）枚举可以提供任意紧的下限。因此，我们得到的第一个证明，决定几乎必然终止（AST）的程序连续分布是$Π^0_2$ -完全的。我们还提供了一个组合表示我们的语义的交叉类型系统。在第二部分中，我们提出了一种证明非仿射程序的AST的方法，即，递归程序，可以在递归体的计算期间，从不同的调用位置进行多次递归调用（一阶函数）。与确定性语言不同，递归调用站点的数量对终止概率有直接影响。我们的框架支持一个证明系统，可以验证AST的程序远远超出了现有方法的范围。我们已经构建了原型实现我们的方法计算下限的终止概率，AST验证。
2021-04-11 cs.LO cs.PL
Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments
具有随机结构的程序是一个活跃的研究课题，特别是在最近引入基于鞅的终止和运行时分析方法之后。与大多数现有的工作，专注于证明几乎肯定终止或估计预期的运行时，在这项工作中，我们研究了运行时的尾部概率，如“执行超过100步的概率最多为1%。“为了这个目标，我们设计了一个上鞅理论，它过度近似了运行时的高阶矩。这些较高的时刻，结合适当的浓度不等式，产生有用的上界的尾部概率。此外，我们的向量值公式使这些上鞅的自动化基于模板的合成。我们的实验表明，该方法的实际用途。
2019-02-15 cs.LO
Supermartingales, Ranking Functions and Probabilistic Lambda Calculus
在连续随机抽样和显式递归的λ演算中，基于排序上鞅，给出了几乎必然终止的一种证明方法。这一结果在三个方面得到了推广。反音排名函数对它们必须下降的速度限制较弱，并且适用于更广泛的程序。稀疏排名函数只在程序可达状态的子集上取值，因此定义起来更简单，也更灵活。排名功能方面的替代减少战略提供了更大的灵活性，并显着增加了适用性的排名上鞅的方法来证明几乎肯定的终止，由于一个新的（限制）合流的结果，这是独立的利益。反调排序函数的概念受到McIver、Morgan、Kaminski和Katoen在一阶命令式语言中的类似工作的启发，但适用于高阶函数式语言。稀疏排名功能和合流语义扩展是唯一的高阶设置。我们的方法可以用来证明几乎肯定终止的程序，是超出了文献中的方法，包括高阶和非仿射递归。
2021-04-30 cs.LO cs.PL
Proving and Disproving Programs with Shared Mutable Data
我们提出了一个工具，用于验证确定性程序与共享的可变引用对规范，如断言，先决条件，后置条件，和读/写效果。我们实现我们的工具编码程序可变引用到注释纯函数递归程序。然后，我们依靠函数展开和SMT求解器Z3来证明或反驳安全性并建立程序终止。我们的工具使用了一种新的程序翻译，其中框架条件使用一阶逻辑中的无量词公式进行编码（而不是依赖于量词或分离逻辑）。这种无量词编码使SMT求解器能够证明安全性或报告相对于过程规范的语义的反例。我们的编码是可能的，这要归功于Z3 SMT求解器的扩展数组理论的表达能力。除了能够报告反例，我们的工具保留了效率的推理纯功能层的数据结构，提供可变数据的表现力，但也是一个显着水平的自动化纯功能方面的软件。我们通过操纵可变链接结构和数组的例子来说明我们的工具。
2021-03-13 cs.LO
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
Why Can't You Behave? Non-termination Analysis of Direct Recursive Rules with Constraints
本文关注的是基于规则的程序出错。规则应用程序的不良行为是计算不终止或失败。我们提出了一个静态的程序分析的非终止性问题的递归约束处理规则（约束处理规则）的语言。是一种涉及约束推理的高级并发声明语言。它与许多其他基于规则的方法密切相关，因此其结果具有更广泛的意义。在这样的语言中，非终止性是由于递归规则的无限应用。失败是由于在计算过程中矛盾约束的积累。我们给出了线性直接递归简化规则的潜在非终止性和失效（以及确定终止性）的具有所谓的不良行为条件的定理。递归规则中约束之间的逻辑关系在这种程序分析中起着至关重要的作用。我们认为，我们的方法可以扩展到其他类型的递归和更一般的一类规则。因此，本文可以作为一个基本的参考和进一步研究的起点。
2017-01-10 cs.LO cs.PL cs.SE
Proceedings International Workshop on Strategies in Rewriting, Proving, and Programming
本卷收录了2010年7月9日在英国爱丁堡举行的第一届重写、证明和编程策略国际研讨会（IWS 2010）的论文集。策略在程序设计语言、自动演绎和推理系统中无处不在。在重写和编程这两个社区，以及演绎和证明引擎（证明者，助手，求解者）这两个社区，已经启动了研讨会，以更深入地理解各种计算和推理系统中策略的性质，它们的描述，它们的属性及其用法。最近，策略在基于重写的程序设计语言、验证工具和技术（如SAT/SMT引擎或终止证明器）中也发挥着重要作用。此外，策略已经被更普遍地看作是表达复杂的设计控制计算，建模，证明搜索，程序转换和访问控制。IWS 2010是作为FLoC 2010的附属讲习班举办的。FLoC 2010提供了一个很好的机会来促进重写和编程社区与演绎和证明引擎社区之间的交流。IWS 2010是自1997年以来举办的两个系列研讨会的联合后续行动：CADE-IJCAR社区举办的战略研讨会和RTA-RDP社区举办的减少战略研讨会。
2010-12-24 cs.LO
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 and Computing: The Infinite Pigeonhole Principle and Countable Choice
University of Oregon（俄勒冈大学）；University of Massachusetts, Lowell（马萨诸塞大学洛厄尔分校）；Université Paris Cité, Inria, CNRS, IRIF（巴黎西岱大学、法国国家信息与自动化研究所、法国国家科学研究中心、IRIF）
本文探讨了结构性共递归在经典推理下的表达能力，通过结合经典调用cc操作符，展示了流处理算法和无限鸽巢原理的证明方法，并实现了可数选择公理的终止性证明。
2026-03-04 cs.LO cs.PL
Loops under Strategies ... Continued
虽然有许多方法可以自动证明术语重写系统的终止性，但到目前为止，只有少数技术可以自动证明其终止性。几乎所有这些技术都试图找到循环，其中循环的存在意味着重写系统的非终止性。然而，大多数程序设计语言使用特定的求值策略，而循环检测技术通常不考虑策略。因此，即使重写系统有一个循环，它仍然可能在某些策略下终止。因此，我们的目标是开发决策程序，可以确定是否一个给定的循环也是一个循环下各自的评估策略。在早期的工作中，这样的程序是为最内层，最外层和上下文敏感的评估策略。在目前的论文中，我们建立在这项工作的基础上，并制定这样的决策程序的重要战略，如最左最内，最左最外，（最大）平行最内，（最大）平行最外，和禁止模式（概括最内，最外，和上下文敏感的战略）。通过这种方式，我们获得了自动反驳这些策略下终止的第一种方法。
2010-12-27 cs.CC cs.LO
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
