Non-termination using Regular Languages
我们描述了一种方法来证明非循环不终止，即长期重写系统不承认循环减少。作为非终止证书，我们采用常规（树）自动机。
2014-05-22 cs.LO
Termination of Triangular Polynomial Loops
研究环 $\mathcal{S}$ 上三角弱非线性循环（twn-loops）的终止性问题，通过将其归约到一阶理论的存在性片段证明可判定性与半可判定性，并提出循环转换、线性化技术及多项式时间的复杂度界限。
2024-02-13 cs.LO
Deciding Termination of Simple Randomized Loops
本文证明了一类由单循环、线性循环条件和两个线性可交换可对角化更新组成的简单随机程序的全称正几乎必然终止性是可判定的，将Tiwari 2004年的研究扩展到随机程序领域。
2025-07-01 cs.LO
Termination of Monotone Programs
我们提出了一个有效的方法来证明终止的单调程序与整数变量，一个表达类的循环，经常遇到的计算机程序。我们的方法是基于一个轻量级的静态分析方法，并利用简单的单调函数的%nice属性。我们的初步实现%beats表明，我们的工具比现有的工具具有优势，可以证明终止一类基准测试的高比例的循环。
2017-02-04 cs.LO
Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)
我们提出了新版本的循环加速工具（LoAT），一个强大的工具，用于证明非终止和最坏情况下的下界程序操作的整数。它是基于一个新的演算循环加速，即，将循环转换为不确定的直线代码，以及用于寻找非终止配置。为了有效地实现它，LoAT使用了一种基于SMT求解和unsat内核的新方法。一项广泛的评估表明，LoAT与其他最先进的证明非终止性的工具相比具有很强的竞争力。虽然没有其他工具能够推导出完整整数规划的最坏情况下的下限，但我们也证明了LoAT的性能显着优于其前辈。
2022-05-16 cs.LO
Disproving (Positive) Almost-Sure Termination of Probabilistic Term Rewriting via Random Walks
RWTH Aachen University（亚琛工业大学）
本文提出首个自动反驳概率项重写系统（正）几乎必然终止性的技术，通过将随机游走嵌入计算来定量分析循环的存在性和计数。
2026-05-28 cs.LO
Non-Termination in Term Rewriting and Logic Programming
本文在统一框架下定义循环与二元链两种非终止形式，提出检测二元链的语法判据，并通过NTI在2023年终止竞赛中与领先分析器比较验证其有效性。
2023-12-21 cs.LO
On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic
本文针对带位向量算术的逻辑约束项重写系统，提出一种基于有向无环图的依赖对处理器，以解决单例自环依赖对问题，并给出无环图存在的充分条件及特定情况下的简化。
2023-07-26 cs.LO
A Calculus for Modular Loop Acceleration and Non-Termination Proofs
循环加速可以用来证明程序的安全性、可达性、运行时界限和（非）终止性。为此，已经提出了各种加速技术。然而，到目前为止，所有这些都是单一的，即，不能使用几种不同加速技术的组合来加速单个循环。相比之下，我们提出了一个演算，允许以模块化的方式结合加速技术，我们展示了如何将许多现有的加速技术集成到我们的演算。此外，我们提出了两种新的加速技术，可以无缝地纳入我们的微积分。其中一些加速技术仅适用于非终止循环。因此，将它们与我们的新演算相结合，产生了一种新的模块化方法来证明非终止性。实证评估表明，我们的方法的适用性，无论是循环加速和证明不终止。
2022-06-08 cs.LO cs.PL
Termination of Real Linear Loops
Swansea University（斯旺西大学）
研究实数上线性和仿射循环的全终止性判定问题，提出部分算法在扰动下稳定，非稳定实例测度为零。
2026-05-01 cs.CC cs.LO
Inference of termination conditions for numerical loops
本文提出了一种新的分析逻辑程序中数值计算终止性的方法。传统的方法由于整数的非良基性而无法对其进行分析。我们提出了一种技术，可以克服这些困难。我们的方法是基于转换程序的方式，允许集成和扩展技术最初开发的数值计算分析的框架中的查询映射对与知名的框架的可接受性。这样的整合不仅有助于理解终止行为的数值计算，但也允许自动执行正确的分析，这样的计算，从而扩展以前的工作基于约束的方法终止。在本文的最后一节中，我们讨论了可能的扩展技术，包括将一般的长期订单。
2001-06-26 cs.LO cs.PL
Efficient Ranking Function-Based Termination Analysis with Bi-Directional Feedback
本文提出终止性分析框架Syndicate，通过双向反馈同时指导排序函数与循环不变量的搜索，在提升可证明终止程序数量的同时降低平均证明时间，性能优于现有工具。
2025-04-08 cs.LO
Termination in Convex Sets of Distributions
本文研究通过单点扩展凸代数以建模概率系统的终止性，完整描述了特定凸代数类（包括分布凸子集代数）及自由凸代数的所有可能扩展，并证明了唯一的函子性黑洞扩展。
2018-11-19 cs.LO
Inference of termination conditions for numerical loops in Prolog
本文提出了一种新的分析逻辑程序中数值计算终止性的方法。传统的方法由于整数的非良基性而无法对其进行分析。我们提出了一种技术，可以克服这些困难。我们的方法是基于转换程序的方式，允许集成和扩展技术最初开发的数值计算分析的框架中的查询映射对与知名的框架的可接受性。这样的整合不仅有助于理解终止行为的数值计算，而且还允许我们自动执行正确的分析，这样的计算，通过扩展以前的工作基于约束的方法终止。最后，我们讨论了可能的扩展的技术，包括将一般术语排序。
2003-07-10 cs.LO cs.PL
Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs
证明程序终止通常通过为程序状态找到有充分根据的排名函数来完成。现有的终止证明器通常使用线性代数或模板来找到排名函数。因此，他们经常被限制在寻找数学整数上的线性排名函数。这类函数不足以证明许多终止程序的终止性，此外，对于数学整数操作的程序的终止参数并不总是导致对于固定宽度机器整数操作的同一程序的终止参数。我们提出了一个终止分析能够产生非线性，字典排序功能和非线性递归集是正确的固定宽度的机器算术和浮点运算我们的技术是基于减少从程序\emph{termination}二阶\emph{satisfaction}。我们提供了配方的终止和非终止在一个片段的二阶逻辑有限域上可判定的限制量化。由此产生的技术是一个健全的和完整的分析有限状态程序的终止固定宽度的整数和IEEE浮点运算。
2014-10-19 cs.LO
Non-Termination of Logic Programs Using Patterns
univ-reunion（留尼汪大学）
本文提出了一种基于模式的逻辑程序非终止性检测方法，通过新展开技术生成无限集合的有限重写序列，并通过实验验证其有效性。
2026-08-10 cs.LO
Proving Termination of Probabilistic Programs Using Patterns
证明程序终止是计算机科学的一个基本挑战。最近的研究已经产生了强大的工具，可以检查各种程序的终止。类似于概率程序，即概率为1的终止（“几乎确定终止”），是随机算法和概率协议同样重要的性质。我们提出了一个新的算法来证明概率程序的几乎必然终止性。我们的算法利用了最先进的模型检查器和终止证明器的非概率程序的力量：它调用这样的工具在一个细化循环，从而迭代地构建一个“终止模式”，这是一组终止运行的概率为1。我们报告各种案例研究，说明我们的算法的有效性。作为进一步的应用，我们的算法可以提高可达概率的下限。
2012-04-13 cs.LO
While Loops in Coq
本文提出在 Coq 浅层嵌入的命令式语言中引入 while 循环的方法，通过一种可定义可能不终止递归函数的通用技术解决 Coq 对终止证明的要求，并以链表程序验证其有效性。
2023-09-25 cs.LO cs.PL
Loops under Strategies ... Continued
虽然有许多方法可以自动证明术语重写系统的终止性，但到目前为止，只有少数技术可以自动证明其终止性。几乎所有这些技术都试图找到循环，其中循环的存在意味着重写系统的非终止性。然而，大多数程序设计语言使用特定的求值策略，而循环检测技术通常不考虑策略。因此，即使重写系统有一个循环，它仍然可能在某些策略下终止。因此，我们的目标是开发决策程序，可以确定是否一个给定的循环也是一个循环下各自的评估策略。在早期的工作中，这样的程序是为最内层，最外层和上下文敏感的评估策略。在目前的论文中，我们建立在这项工作的基础上，并制定这样的决策程序的重要战略，如最左最内，最左最外，（最大）平行最内，（最大）平行最外，和禁止模式（概括最内，最外，和上下文敏感的战略）。通过这种方式，我们获得了自动反驳这些策略下终止的第一种方法。
2010-12-27 cs.CC cs.LO
Positive Almost-Sure Termination of Polynomial Random Walks
本文针对概率程序终止性问题，证明步长随迭代多项式增长、分支概率恒定的多项式随机游走满足正几乎必然终止（PAST）的条件，并通过结合遗传规划等方法实现了相关阈值的近似。
2025-06-17 cs.LO
Termination of linear loops under commutative updates
本文研究交换可逆矩阵更新下多路径线性循环的终止性判定问题，通过将其转化为多项式环与多项式半环上模中是否存在正元素的代数问题，证明了该问题是可判定的。
2023-04-19 cs.LO math.RA
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
The 2-Dimensional Constraint Loop Problem is Decidable
本文证明二维实数域上由线性约束合取定义的循环终止（等价于相应二元关系的良基性）问题可判定。
2024-04-26 cs.LO
Ghost Signals: Verifying Termination of Busy-Waiting (Extended Version)
多处理器机器的程序通常执行忙等待同步。我们提出了第一个分离逻辑模块化验证终止的公平调度下，这样的程序。我们的逻辑要求证明作者将虚信号与每个忙等待循环相关联，并允许这样的循环在其相应的信号$s$未设置时停止。证明作者还必须对信号定义有根据的顺序，并证明如果循环线程持有设置信号$s^\prime$的义务，则$s^\prime$的顺序高于$s$。通过使用传统的共享状态不变量将重影信号的状态与数据结构的状态相关联，可以验证在任意数据结构上忙等待任意条件的程序。
2021-05-18 cs.LO cs.PL
Almost-Sure Termination by Guarded Refinement
本文提出Caliper，一种基于受保护递归和概率耦合的高阶分离逻辑，通过证明程序与简单模型间的精化来建立概率程序的几乎必然终止，并在Coq中验证多个示例。
2024-11-11 cs.LO cs.PL
On Deciding Constant Runtime of Linear Loops
RWTH Aachen University（亚琛工业大学）；University of Sussex（萨塞克斯大学）
本文研究了线性循环在实数或有理数范围内运行时间是否为常数的判定问题，并提出了相关算法及实现。
2026-01-13 cs.LO
Non-Termination Inference of Logic Programs
本文提出了一种逻辑程序非终止推理的静态分析技术。我们的框架依赖于包容测试的扩展，其中一些特定的参数位置可以被实例化，而另一些则被泛化。我们给出的语法标准，静态地确定这样的参数位置从一个程序的文本。原子左循环查询从感兴趣的程序的二进制展开的选定子集自底向上生成。我们提出了一套正确的算法自动化的方法。然后，非终止推理是定制的，试图证明左终止条件计算的终止推理工具的最优性。实验评估报告。当终止性和非终止性分析为逻辑过程产生互补的结果时，则相对于最左边的选择规则和用于描述原子查询集的语言，每个分析都是最优的，并且它们一起引起逻辑过程的操作行为的表征。
2004-06-22 cs.LO cs.PL
O-Minimal Invariants for Discrete-Time Dynamical Systems
线性回路的终止性分析在计算机科学的许多领域中起着关键作用，包括程序验证和抽象解释。对于线性循环的最简单的变体，终止问题已经涉及到数论中的深开放问题，例如线性递归序列的Skolem和Positivity问题的可判定性，或者离散时间线性动力系统的等价可达性问题。在本文中，我们介绍了类的\emph{o-minimal invariants}，这是广泛的比以前考虑的，并研究了可判定性的存在和算法合成等不变量作为证书的非终止线性循环配备了一大类的停机条件。我们建立了两个主要的可判定性结果，其中一个条件Schanuel的猜想在超越数论。
2020-05-11 cs.CC cs.LO math.AG
Verifying Termination of General Logic Programs with Concrete Queries
我们介绍了一种方法来验证终止逻辑程序相对于具体的查询（而不是抽象的查询模式）。建立了一个充分必要条件，并提出了一种自动验证算法。与现有的基于查询模式的方法相比，我们的方法具有以下特点：（1）它适用于所有一般的逻辑程序与非挣扎查询。(2)它非常容易自动化，因为它不需要搜索级别映射或模型，也不需要基于额外的模式或类型信息计算参数间关系。(3)它桥接了终止分析与循环检查，这两个问题在过去已经被单独研究，尽管它们彼此之间有着密切的技术关系。
2000-06-21 cs.AI cs.LO
A shallow dive into the depths of non-termination checking for C programs
针对现有非终止性检查工具在现实程序上效果不佳的问题，提出一种基于有界模型检查的健全高效技术，通过循环内断言与迭代展开深度检查循环状态，实验表明优于现有工具。
2024-09-04 cs.LO cs.SE
Ranking Templates for Linear Loops
提出了一种基于线性排序模板的线性循环程序终止参数约束综合的新方法。线性排序模板是参数化的、有良好基础的关系，使得对参数的分配产生排序函数。这种方法概括了现有的方法，使我们能够使用模板的许多不同的排名功能与仿射线性组件。我们讨论模板多相，分段，字典排序功能。由于这些排序模板需要严格和非严格的不等式，我们使用Motzkin的换位定理，而不是法卡斯引理转换生成的$\exists\forall$ -约束到一个$\exists$ -约束。
2014-01-21 cs.LO
Deciding Conditional Termination
我们解决的问题，有条件终止，这是一个给定的程序总是终止定义的初始配置集。首先，我们定义的对偶集，从一个非终止执行存在的初始配置，作为最大的不动点的功能，映射到其原像的一组状态的过渡关系。这个定义允许计算最弱的非终止前提条件，如果至少有以下之一成立：（i）转移关系是确定性的，（ii）降阶Kleene序列过逼近最大不动点收敛于100步，或（iii）转移关系是有根据的。我们证明了两类关系（即八边形和有限么半群仿射关系）都是这种情况。此外，由于这些关系的封闭形式可以在Presburger算法中定义，我们得到了这种循环的终止问题的可判定性。
2014-08-20 cs.FL cs.LO
Modular Verification for Almost-Sure Termination of Probabilistic Programs
在这项工作中，我们考虑几乎肯定终止问题的概率程序，询问是否一个给定的概率程序终止概率为1。可伸缩的程序分析方法通常依赖于模块化作为其理论基础。在非概率程序中，Floyd-霍尔逻辑的经典变式规则（V-规则）为模块化分析提供了基础。将该规则扩展到概率程序的几乎确定终止是相当棘手的，并且在[Fioriti and Hermanns 2015]中提出了一个概率变体。虽然所提出的概率变量谨慎地解决了可积性的关键问题，我们表明，所提出的模块化规则仍然是不健全的几乎肯定终止的概率程序。除了建立以前的规则的不健全，我们的贡献如下：首先，我们提出了一个健全的模块规则几乎确定终止的概率程序。我们的方法是基于一个新的概念下降上鞅。其次，对于算法方法，我们考虑下降上鞅是线性的，并表明它们可以在多项式时间合成。最后，我们提出了各种基准测试和几个自然的例子，模拟各种类型的嵌套而循环的概率程序的实验结果，并证明我们的方法是能够有效地证明其几乎肯定的终止属性。
2019-08-12 cs.LO cs.PL
Ranking Templates for Linear Loops
提出了一种基于线性排序模板的线性循环程序终止参数约束综合的新方法。线性排序模板是参数化的、有良好基础的关系，使得对参数的分配产生排序函数。我们的方法概括了现有的方法，使我们能够使用模板的许多不同的排名功能与仿射线性组件。我们讨论模板多相，嵌套，分段，并行和字典排序功能。这些排名模板可以组合成更强大的模板。由于这些排序模板需要严格和非严格的不等式，我们使用Motzkin的换位定理，而不是法卡斯引理转换生成的$\exists\forall$ -约束到一个$\exists$ -约束。
2015-03-29 cs.LO
On the Termination of Linear and Affine Programs over the Integers
整数上仿射规划的终止性问题在\cite{Braverman}中一直没有解决。十多年来，它一直被认为是一个具有挑战性的开放问题。据我们所知，我们在这里提出了最完整的回应这个问题：我们表明，终止仿射程序在Z是可判定的假设下，几乎所有的仿射程序，除了一个非常小的类零Lesbegue措施。对于环Z上的线性循环规划，我们使用了渐近非终止初始变量值的概念。这些值直接与初始变量值相关联，对于这些初始变量值，相应的程序不会终止。我们减少了整数上的线性仿射规划的终止问题，一个特定的ANT集的初始变量值的空检查。对于这类线性或仿射规划，我们证明了相应的ANT集是一个半线性空间，我们提供了一个强大的计算方法，允许自动生成这些$ANT$集。此外，我们也可以解决条件终止问题。换句话说，通过采用ANT集补，我们获得了程序确实终止的输入集的精确欠近似。
2014-09-18 cs.DM cs.LO
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
Automated Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops (Short WST Version)
本研究提出一种模块化方法，将三角弱非线性循环的运行时间界研究成果用于整数程序复杂度分析，通过计算子程序局部界并提升为全局界，实现了现有顶尖工具无法完成的复杂度分析。
2023-07-19 cs.LO
Neural Termination Analysis
University of Birmingham（伯明翰大学）；Amazon, Inc.（亚马逊公司）；University of Oxford（牛津大学）
我们介绍了一种新的方法来自动终止分析的计算机程序：我们使用神经网络来表示排名功能。排名函数将程序状态映射到从下到上有界的值，并随着程序的运行而减少;排名函数的存在证明程序终止。我们训练一个神经网络从采样的执行轨迹的程序，使网络的输出沿轨迹减少，然后，我们使用符号推理正式验证，它概括到所有可能的执行。在肯定的答案，我们获得一个正式的证书终止程序，我们称之为神经排名功能。我们证明，由于神经网络的能力，代表非线性函数，我们的方法成功的程序，是超出了国家的最先进的工具。这包括在循环条件中使用析取的程序和包含非线性表达式的程序。
2022-09-06 cs.LG cs.LO cs.PL
Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
本文提出一种模块化方法，将子程序转换为 twn-loops 计算局部运行时间界限并提升为全局界限，在工具 KoAT 中实现了对其他最先进工具无法处理的整数程序的复杂度分析。
2024-11-15 cs.LO
New results on rewrite-based satisfiability procedures
程序分析和验证需要决策过程根据数据结构的理论进行推理。理论T中的许多问题都可以归结为基文字集的可满足性问题。如果一个可靠的完备的一阶逻辑推理系统保证在T-可满足性问题上终止，那么使用该系统和公平搜索计划的任何定理证明策略都是T-可满足性过程。我们证明了基于重写的一阶引擎的终止记录，整数偏移量，整数偏移模和列表的理论。我们给出了一个模块性定理，说明终止理论的组合的充分条件，每个终止。上述理论以及其他理论都满足这些条件。我们介绍了这些理论及其组合的几套基准测试，包括参数合成基准测试的可扩展性，和现实世界的问题，以测试性能的巨大的文字集。我们比较重写的定理证明器E与有效性检查器CVC和CVC Lite。与通用证明器无法与具有内置理论的推理机竞争的民间传说相反，实验总体上有利于定理证明器，表明重写方法不仅优雅且概念简单，而且具有重要的实际意义。
2008-06-01 cs.AI cs.LO
Ranking Functions for Linear-Constraint Loops
本文研究整数变量线性约束循环中线性及字典序线性排序函数的存在性问题，证明一般情形为 coNP 完全，识别 PTIME 特例并给出完整综合算法。
2025-09-29 cs.LO cs.PL
On the Complexity of the Escape Problem for Linear Dynamical Systems over Compact Semialgebraic Sets
本文研究了紧半代数集上离散线性动力系统的逃逸问题的计算复杂性，或者等价地研究了具有紧半代数保护集的仿射回路的终止问题.考虑由无否定的$\exists \forall$ -句子组成的不含严格不等式的实数理论的片断。我们得到几个等价的表征相关的复杂性类，证明其鲁棒性，并说明其表达能力。我们表明，紧凑的逃逸问题是完全的这个类。
2021-07-05 cs.CC cs.LO
Synthesis for Polynomial Lasso Programs
我们提出了一种方法的多项式套索程序的综合。这些程序由一个程序干、一组转换和一个退出条件组成，所有这些都以代数断言（多项式等式的合取）的形式出现。这种方法的核心是发现非线性（代数）循环不变量。我们扩展Sankaranarayanan，Sipma，和曼纳的基于模板的方法，并证明了一个完整的标准。我们执行程序合成通过生成一个约束，其解决方案是一个合成的程序与循环不变，证明程序的正确性。此约束是非线性的，并传递给SMT求解器。此外，我们可以强制终止的合成程序的测试用例的支持。
2013-11-16 cs.LO
A New Proof Rule for Almost-Sure Termination
概率程序的一个重要问题是它所有发散运行的概率质量是否为零，也就是说它“几乎必然”终止。证明这一点可能很难，本文提出了一种新的方法来做到这一点;它是在程序逻辑中表达的，因此直接适用于源代码。程序可能包含概率选择和恶魔选择，概率选择可能取决于当前状态。和其他研究人员一样，我们使用变量函数（也称为变量函数）。“超鞅”）是实值的，并且在每次循环迭代中概率可能会减少;但我们的关键创新在于减少的数量和概率是参数的。我们证明了新的规则的合理性，表明其适用性超出现有的规则，并解释其连接到经典的结果可数（非恶魔）马尔可夫链。
2017-12-26 cs.LO cs.PL
Generating Asymptotically Non-Terminating Initial Values for Linear Programs
提出了线性循环规划的渐近非终止初始变量值的概念。这些值直接与初始变量值相关联，对于这些初始变量值，相应的程序不会终止。我们的理论贡献为我们提供了强大的计算方法，自动生成一套渐近非终止的初始变量值。这样的集合由半线性空间符号地和精确地表示，例如，以线性等式和不等式的合取和析取为特点。此外，通过取它们的补码，我们得到了程序终止的输入集的精确欠近似。然后我们可以把线性规划的终止问题归结为一组特定的渐近非终止初始变量值的空性检查。我们的静态输入数据分析不仅限于程序中的变量解释的实数。我们扩展了我们的方法，并提供了新的可判定性结果的仿射整数和理性规划的终止问题。
2014-08-15 cs.DM cs.LO
An early sign of satisfiability
本文考虑命题子句集（SAT实例）的可满足性检查。结果表明，在求解SAT问题的过程中，子句的“单极集”（不包含肯定子句或否定子句）在所有子句满足之前提供了SAT实例可满足性的“早期信号”.在这个符号处，处理可以通过“单极集合终止”来终止，因此在它通常由SAT求解器完成之前UST（表1）。对SAT竞赛中使用的基准SAT实例的分析表明，UST可以加快解决源于许多现实问题的SAT实例。UST的效率随着被检查的SAT集合的“偏度”而增加，该偏度是集合中否定和非否定文字的概率之间的差异。许多现实世界的问题，由于它们的语义，是扭曲的（表2）。UST的效率可以通过揭示SAT集合的“隐藏偏度”来提高（表3）。
2016-12-15 cs.LO
Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs
本文提出了一个wp风格的演算获得的概率程序的期望运行时间的界限。它的应用包括确定（可能无限）的期望终止时间的概率程序和证明积极的几乎必然终止-一个程序终止概率1在有限的期望时间？我们提供了几个证明规则的运行时间的循环，并证明了一个简单的操作模型的方法的可靠性。我们表明，我们的方法是一个保守的扩展Nielson的方法推理确定性程序的运行时。我们分析了一些示例程序的预期运行时间，包括一维随机游走和优惠券收集器问题。
2017-11-28 cs.LO cs.PL
Verification of Nondeterministic Quantum Programs
非确定性选择是一种有用的程序构造，它提供了一种描述程序行为的方法，而无需指定可能实现的细节。它支持程序的逐步细化，这是一种在软件开发中被证明有用的方法。非确定性也被引入到量子编程中，非确定性量子程序的终止已经被广泛分析。在本文中，我们超越了终止分析，研究非确定性量子程序的验证，其中属性由相关的希尔伯特空间上的厄米算符集给出。Hoare型逻辑系统的部分和全部的正确性提出，这原来是既健全和相对完整的，就其相应的语义正确性。为了展示这些证明系统的实用性，我们分析了一些量子算法，如量子纠错方案，Deutsch算法和非确定性量子行走。最后，实现了一个证明助手原型，以帮助非确定性量子程序的自动推理。
2023-02-15 cs.LO quant-ph
Formalizing Wu-Ritt Method in Lean 4
Shandong University（山东大学）；Academy of Mathematics and Systems Science, University of Chinese Academy of Science（中国科学院数学与系统科学研究院）；Sun Yat-sen University（中山大学）
本文在Lean 4中形式化了吴-里特特征集方法，涵盖多项式初式、顺序、伪除法等核心概念，并验证了基本集、特征集及零分解算法的终止性和正确性。
2026-04-16 cs.LO math.AC
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
Loop Formulas for Description Logic Programs
Guizhou University（贵州大学）；University of Alberta（阿尔伯塔大学）
Eiter等人提出的描述逻辑程序（DL-programs）为语义Web提供了一种简洁而强大的形式化方法，用于集成回答集编程和描述逻辑。本文将逻辑程序的完备化和循环公式的概念推广到描述逻辑程序，并证明了dl-程序的完备化和循环公式的模型可以精确地捕捉到dl-程序的回答集。此外，我们提出了一个新的，替代的语义DL-程序，称为{ \em规范答案集语义}，这是由模型定义的完成，满足所谓的规范循环公式。规范答案集的一个理想性质是它们没有循环论证。本文还探讨了规范答案集的一些性质。
2010-07-23 cs.AI cs.LO
2LS: Heap Analysis and Memory Safety (Competition Contribution)
2LS是一个分析顺序C程序的框架，可以验证和反驳程序断言和终止。2LS框架建立在CPROVER基础设施之上，并实现了基于模板的合成技术，例如找到不变量和排名函数，以及增量循环展开技术来找到反例和k-归纳证明。今年版本的主要改进是2LS分析程序的能力，这些程序需要对动态数据结构的形状和内容进行组合推理，以及用于存储器安全属性的仪器。
2020-01-03 cs.LO cs.SE
BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems
本文提出BURNS算法，通过过近似系统动力学并求解混合整数线性规划来计算神经反馈环的欠近似后向可达集，从而验证目标可达性，扩展了学习使能系统的可验证性质范围。
2025-05-06 cs.AI cs.LO cs.SY
