Polytool: polynomial interpretations as a basis for termination analysis of Logic programs
我们的目标是研究移植终止分析技术开发的一个编程范式到另一个范式的可行性。在本文中，我们将展示如何适应终止分析技术的多项式解释的基础上-非常有名的术语重写系统（TRS）的背景下-获得新的（非转换）的终结分析技术，明确的逻辑程序（LP）。这导致了一种方法，可以被看作是一个直接推广的传统技术在终止分析的LP，线性规范和水平映射。我们的扩展一般化这些任意多项式。我们扩展了一些标准的概念和结果终止分析的上下文多项式的解释。我们还提出了一个基于约束的方法自动生成多项式的解释，满足终止条件。基于这种方法，我们实现了一个新的工具，称为Polytool，自动终止分析的LP。
2009-12-22 cs.LO cs.PL
On Modular Termination Proofs of General Logic Programs
该研究提出一种基于可接受程序概念的模块化方法，可通过单独处理层级模块证明含否定的通用逻辑程序终止性，针对良模式、良类型程序给出验证技术与迭代证明法，能大幅简化证明。
2001-07-30 cs.LO cs.PL
A Dynamic Approach to Characterizing Termination of General Logic Programs
本文给出了一般逻辑程序终止性的一个新的刻画。大多数现有的终止分析方法依赖于关于逻辑程序的源代码的结构的一些静态信息，诸如模式/类型、范数/级别映射、模型/参数间关系等。我们提出了一个动态的方法，它采用了一些关键的动态功能的无限（广义）SLDNF衍生，如重复选定的子目标和递归增加长期的大小。我们还介绍了一种新的制定SLDNF树，称为广义SLDNF树。广义SLDNF-树以与Prolog相同的方式处理负子目标，并且存在于任何一般逻辑程序中。
2002-04-12 cs.LO cs.PL
An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear $π$-Calculus
公平终止是程序的属性，这些程序可能“在原则上”偏离，但“在实践中”终止，即在关于非确定性选择的解决方案的适当公平假设下终止。我们研究了$μ$ MALL $^\infty$的一个保守扩展，$^\infty$是线性逻辑中具有最小和最大不动点的乘性加性片段的无穷证明系统，使得割消对应于公平终止。证明项是$π$ LIN的过程，它是线性$π$演算的一个变体，具有（共）递归类型，可以将二进制和（某些）多方会话编码到其中。因此，我们获得了一个行为类型系统的$π$ LIN（和间接会话演算通过其编码到$π$ LIN），确保公平终止：虽然良好的类型的进程可能会参与任意长的交互，他们是公平的保证，最终执行所有挂起的动作。
2022-07-08 cs.LO cs.PL
Verifying Termination and Error-Freedom of Logic Programs with block Declarations
我们提出了延迟声明的逻辑程序的验证方法。验证的性质是终止和自由的错误有关的内置。关于终止，我们提出了两种方法。第一种方法试图消除众所周知的推测性输出绑定问题。第二种方法是基于识别的谓词，使用这个谓词的原子的文本位置是无关的终止。这项工作有三个特点：它允许在几种模式下使用谓词;它表明块声明，这是一个非常简单的延迟结构，足以确保所需的属性;它考虑到选择规则，假设它是在大多数Prolog实现。这些方法可用于验证现有程序和帮助编写新程序。
2000-06-23 cs.LO cs.PL
Termination Prediction for General Logic Programs
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所计算机科学国家重点实验室）；Department of Computer Science, Celestijnenlaan 200 A, B-3001 Heverlee, Belgium（计算机科学系）
我们提出了一个启发式的框架攻击的不可判定终止问题的逻辑程序，作为一种替代目前的终止/非终止证明方法。我们引入了终止预测的思想，它预测终止的逻辑程序的情况下，无论是终止或非终止证明是适用的。我们建立了一个必要和充分的表征无限（广义）SLDNF-衍生任意（具体或moded）查询，并开发了一个算法，预测终止一般逻辑程序与任意非floundering查询。我们已经实现了一个终止预测工具，并取得了相当满意的实验结果。除了5个程序打破了实验时间限制，我们的预测是100%正确的所有296个基准程序的终止竞争2007年，其中18个程序不能证明任何现有的国家的最先进的分析仪，如AProVE 07，NTI，Polytool和TALP。
2009-05-13 cs.AI cs.LO cs.PL
Automated Termination Proofs for Logic Programs by Term Rewriting
RWTH Aachen（亚琛工业大学）；TU Eindhoven（埃因霍温理工大学）；University of Innsbruck（因斯布鲁克大学）
逻辑程序的可终止性分析有两种方法：“转换”法和“直接”法。直接方法直接在逻辑程序的基础上证明终止。转换方法将一个逻辑程序转换成一个项重写系统（TRS），然后分析所得到的TRS的终止。因此，转换方法使以前为TRS开发的所有方法也可用于逻辑程序。然而，大多数现有的转换的适用性是相当有限的，因为它们只能用于逻辑程序的某些子类。(Most它们中的一个仅限于模式良好的程序。）在本文中，我们改进这些转换，使它们成为适用于任何明确的逻辑程序。为了用TRS模拟逻辑程序的行为，我们稍微修改了重写的概念，允许无限项。我们表明，我们的转换结果TRS这确实是适合自动终止分析。与大多数其他逻辑程序的终止方法相比，我们的技术也适用于逻辑程序设计，而不需要发生检查，这是在实践中通常使用的。我们在终止证明程序AProVE中实现了我们的方法，并在大量示例中成功地对其进行了评估。
2008-09-01 cs.AI cs.LO cs.PL
Modular termination verification with a higher-order concurrent separation logic (Intermediate report)
我们报告的中间结果，我们的研究推理活性属性，除了深正确性的一个命令，并发程序设计语言与高阶存储。目前，我们集中在一个特定的活性属性，即终止。通过保证终止性，我们可以将部分正确性的陈述加强为完全正确性。这是通过将终止性转换为安全属性的经典方法来实现的。特别是，我们扩展的程序设计语言考虑与调用权限，这已被证明，使模块化的推理终止。添加原子块是为了增加我们基于调用权限的方法的表现力。我们的工作建立在Iris --一个基础的、机器检查的、高阶并发分离逻辑框架--之上，而不修改它。有了这些补充，我们就能够模块化地推理并发但非阻塞算法的终止。我们对正在考虑的程序设计语言的添加保留了Iris对帮助和预言进行推理的能力。作为一个例子，我们将当前的系统应用于现有的无锁并发堆栈的案例研究，并在Iris中得到了证明。最后，我们概述了扩展阻塞并发方法的后续步骤。
2022-12-28 cs.LO cs.PL
Automatic Termination Analysis of Programs Containing Arithmetic Predicates
对于带有算术谓词的逻辑程序，显示终止并不容易，因为整数的通常顺序并没有充分的根据。一种新的方法，很容易纳入TermiLog系统的自动终止分析，在这种情况下，显示终止。该方法包括以下步骤：首先，自动推导出表示整数值域的有限抽象域。在此基础上，对程序进行抽象解释.其结果是一个有限数量的原子抽象的答案查询，用于扩展查询映射对的技术。对于每个潜在非终止的查询映射对，猜测有界（整数值）终止函数。如果遍历该对减少了终止函数的值，则建立终止。简单的函数通常足以满足每个查询映射对，这使我们的方法比传统方法更有优势，传统方法对所有循环使用单个终止函数，这必然会更复杂，更难自动猜测。值得注意的是，McCarthy的91函数的终止可以使用我们的方法自动显示。总之，所提出的方法是基于结合的查询映射对的技术的整数的有限抽象，并且基本上是能够划分为几种情况下，这样一个简单的终止功能足以为每种情况下的终止证明。因此，证明终止的整个过程可以在TermiLog和类似系统的框架内自动完成。
2000-11-23 cs.PL
Inferring Termination Conditions for Logic Programs using Backwards Analysis
本文主要研究保证逻辑程序终止的模式的推理。这概括了传统的端接分析，其中分析仪试图验证指定模式的端接。我们的贡献是一种方法，其中传统的终止分析的组成部分相结合，向后分析，以获得终止推理的分析。我们确定了一个条件的组件的分析，保证终止推理将推断出所有的模式，可以检查终止。这种方法的应用，以提高传统的终止分析，也终止推理进行演示。
2003-12-12 cs.PL
Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling
在逻辑编程中，动态调度是指在运行时确定每个解析（计算）步骤中原子的选择的情况，而不是像Prolog中从左到右的选择规则。这在例如并行编程中具有应用。在现有的语言中，以延迟声明的形式提供了一种控制动态调度的机制。在抽象技术细节的同时，引入了消耗输入的推导来描述动态调度。在本文中，我们首先正式延迟声明和输入消费派生之间的关系，在许多情况下，一对一的对应关系。然后，我们定义了一个模型理论的语义输入消费派生的简单模式的程序。最后，对于这类程序，我们提供了一个终止的充分必要条件。
2001-01-23 cs.LO cs.PL
Reflections on Termination of Linear Loops
本文展示了如何线性动力系统的技术可以用来推理一般循环的行为。我们提出了两个主要结果。首先，我们证明了每一个可以表示为线性整数运算中的转换公式的循环都有一个最佳模型作为确定性仿射转换系统。其次，我们证明了，对于任何线性动力系统$f$与整数特征值和任何整数算术公式$G$，有一个线性整数算术公式，恰好为$G$的状态，其中$f$最终不变。结合这两个，我们开发了一个单调的条件终止分析一般循环。
2021-05-28 cs.PL
A Non-Termination Criterion for Binary Constraint Logic Programs
一方面，逻辑程序的终止性分析现在是逻辑编程社区中一个相当成熟的研究课题。另一方面，非终止性分析似乎仍然是一个不太吸引人的主题。如果把这条研究路线分为动态分析和静态分析两种方法，本文属于后者。它提出了一个标准，检测非终止原子查询的二进制CLP规则，严格概括了我们以前的工作在这个问题上。我们给出了一个通用的操作定义和实现的逻辑形式，这个标准。然后，我们证明了逻辑形式是正确的和完整的操作定义。
2009-01-10 cs.PL
Termination analysis of logic programs using acceptability with general term orders
提出了一种新的逻辑程序终止性分析方法。该方法的本质是，我们利用一般的术语排序（而不是级别映射），就像在逻辑程序终止分析的转换方法中所做的那样，但是我们将这些排序直接应用于逻辑程序，而不是通过一些转换获得的术语重写系统。我们定义了一些变量的可接受性，一般术语排序的基础上，并显示它们是如何等同于LD-终止。我们开发了一个需求驱动的，基于约束的方法来验证这些可接受的变量。该方法优于标准可接受性的优点是，在某些情况下，需要复杂的级别映射，可以很容易地生成相当简单的术语排序。与转换方法相比，它的优点是完全避免了转换步骤。
2000-11-17 cs.PL
An Improved Non-Termination Criterion for Binary Constraint Logic Programs
一方面，逻辑程序的终止性分析现在是逻辑编程社区中一个相当成熟的研究课题。另一方面，非终止性分析似乎仍然是一个不太吸引人的主题。如果把这条研究路线分为动态分析和静态分析两种方法，本文属于后者。它提出了一个标准，检测非终止原子查询的二进制CLP条款，严格概括了我们以前的工作在这个问题上。我们给出了这一准则的一般操作定义和逻辑形式。然后，我们证明了逻辑形式是正确的和完整的操作定义。
2005-08-24 cs.PL
On termination of meta-programs
术语{ \em元编程}指的是编写将其他程序作为数据并利用其语义的程序的能力。本文的目的是提出一种方法，使我们能够执行一个正确的终止分析广泛的实用元解释器，包括否定和执行不同的任务在执行过程中。它是基于结合的权力，一般秩序，用于证明终止的长期重写系统和程序，并在著名的可接受性条件，用于证明终止的逻辑程序。该方法建立证明解释程序的终止所需的排序与证明元解释器连同该解释程序的终止所需的排序之间的关系。如果建立了这种关系，其中一个关系的终止意味着另一个关系的终止，即，元解释器保留终止。在元解释器中，正确分析的是构造元解释器的证明树，不同类型的跟踪器和推理器。不带附录出现在逻辑程序设计理论与实践中。
2003-12-24 cs.LO cs.PL
Non-termination of Dalvik bytecode via compilation to CLP
我们提出了一套规则编译Dalvik字节码程序到一个逻辑程序与数组约束。结果程序的非终止性包含了原程序的非终止性，因此我们以前提出的证明约束逻辑程序的非终止性的方法也可用于证明Dalvik程序的非终止性.
2014-12-10 cs.PL
Acceptability with general orderings
提出了一种新的逻辑程序终止性分析方法。该方法的本质是我们使用一般的排序（而不是级别映射），就像在逻辑程序终止分析的转换方法中所做的那样，但是我们将这些排序直接应用于逻辑程序，而不是通过一些转换获得的术语重写系统。我们定义了一些变量的可接受性，一般的排序的基础上，并显示它们是如何等同于LD-终止。我们开发了一个需求驱动的，基于约束的方法来验证这些可接受的变量。该方法优于标准可接受性的优点是，在某些情况下，需要复杂的级别映射，可以很容易地生成相当简单的排序。与转换方法相比，它的优点是完全避免了转换步骤。{ \bf Keywords：}终止分析、可接受性、排序。
2001-06-26 cs.LO cs.PL
A General Framework for Automatic Termination Analysis of Logic Programs
本文描述了一个逻辑程序自动终止分析的一般框架，其中我们用“终止”来理解为程序和给定查询构造的LD树的有限性。证明了无限LD-树的分支的某个子集到有限集的映射的一个一般性质。从这一结果导出几个终止定理，通过使用不同的有限集。前两个是制定谓词依赖和原子依赖图。然后证明了与程序相关的查询-映射对的一般结果（参见图1）。\cite{Sagiv,Lindenstrauss:Sagiv}）。在\cite{Lindenstrauss:Sagiv:Serebrenik}中描述的{ \em TermiLog}系统的正确性由此而来。在这个系统中，不可能证明涉及算术谓词的程序的终止性，因为整数的通常顺序不是有根据的。本文提出了一种新的方法，它可以很容易地结合在{ \em TermiLog}或类似的系统中，这使得它有可能证明终止程序涉及算术谓词。它是基于一个有限的整数抽象与查询映射对的技术相结合，基本上是能够划分为几种情况下，这样一个简单的终止功能足以为每种情况下的终止证明。最后概述了几种可能的扩展。
2000-12-13 cs.PL
On the Fair Termination of Client-Server Sessions
客户-服务器的【形】会话基于线性逻辑命题作为会话类型的传统解释的变体，其中非线性通道（调节客户端池和单个服务器之间的交互的通道）由共指数而不是通常的指数来类型化。共指数能够对竞争交互进行建模，从而客户端竞争与单个服务器进行交互，该服务器的内部状态（以及所提供的服务）可能会随着服务器顺序处理请求而发生变化。在这项工作中，我们提出了一个公平的终止结果CSLL $^\infty$，客户-服务器的【形】会话的核心演算。我们设计了一个类型系统，使得每个类型良好的术语对应于$μ$ MALL $^\infty$中的一个有效推导，$^\infty$是线性逻辑的最小和最大不动点的无穷证明理论。然后，我们建立了一个对应关系之间的减少在微积分和主要减少在$μ$ MALL $^\infty$。CSLL $^\infty$中的公平终止来自$μ$ MALL $^\infty$中的切割消除。
2022-12-11 cs.LO cs.PL
Almost-Sure Termination by Guarded Refinement
本文提出Caliper，一种基于受保护递归和概率耦合的高阶分离逻辑，通过证明程序与简单模型间的精化来建立概率程序的几乎必然终止，并在Coq中验证多个示例。
2024-11-11 cs.LO cs.PL
Synthesis of models for order-sorted first-order theories using linear algebra and constraint solving
声明性程序终止分析的最新发展强调使用适当的模型作为一种通用的方法来证明声明性程序的终止性的逻辑理论代表的程序处于危险之中。在这种情况下，顺序排序的一阶逻辑提供了一个强大的框架来表示声明性程序。它还提供了一个目标逻辑，以通过转换获得其他逻辑的模型。我们研究了顺序排序的一阶逻辑的数值模型的自动生成及其在程序分析中的应用，特别是在声明式程序的终止分析中。我们使用凸域给域的不同种类的顺序排序的签名，我们解释排序的签名通过适当适应凸矩阵的解释排名的符号。这种数值解释允许使用现有的算法和工具，从线性代数和算术约束求解合成的模型。
2015-12-22 cs.LO cs.PL
Fair Termination of Asynchronous Binary Sessions
本文提出基于线性逻辑的异步会话类型理论，利用新颖的公平异步子类型关系保证良类型进程在公平性假设下公平终止，实现无饥饿与无孤儿消息。
2025-03-14 cs.DC cs.LO cs.PL
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs
我们提出了TaDA现场，一个并发分离逻辑的推理组合终止阻塞细粒度并发程序。关键的挑战是如何处理抽象的原子阻塞：也就是说，抽象的原子操作具有阻塞行为，这些阻塞行为来自于例如细粒度自旋锁中的忙等待模式。我们的基本创新是抽象规范的设计，捕捉这种阻塞行为作为对环境的活跃假设。我们设计了一个逻辑，可以原因的客户端使用这些操作的终止，而不会打破他们的抽象边界，和操作的实现相对于他们的抽象规范的正确性。我们引入了一个新的语义模型，使用分层的主观义务来表达活性不变量，和一个证明系统，这是健全的模型。我们的规范和推理的微妙之处说明了使用几个案例研究。
2021-11-30 cs.LO cs.PL
Better Termination for Prolog with Constraints
实际的Prolog系统的终止性是脆弱的，难以分析。缺乏发生检查，moded和过载的算术评价通过是/2和偶尔nontermination的有限域约束是无效的终止分析器，依赖于理想化的假设所获得的终止结果的所有来源。在本文中，我们提出的解决方案，以解决这些问题的底层Prolog系统的水平。改进的统一模式通过提供动态发生检查检测来满足基于范数的分析器的要求。广义有限域求解器克服了传统算法的缺点，没有显着的运行时开销。解算器提供无界域，但传播始终终止。我们的工作改进了Prolog的终止性，使Prolog成为一个更可靠的终止性和类型分析的目标。它是SWI-Prolog 5.6.50版本的一部分。
2009-03-12 cs.PL cs.SE
cTI: A constraint-based termination inference tool for ISO-Prolog
我们提出了cTI，第一个系统的通用左终止推理的逻辑程序。终止性推理推广了终止性分析和检验。传统上，终止分析器试图证明给定类的查询终止。这个类必须提供给系统，例如通过用户注释的方式。此外，每次更新感兴趣的查询类时，都必须重新进行分析。相反，终止推理既不需要用户注释，也不需要重新计算。在这种方法中，立即推断所有谓词的终止类。我们描述了CTI的体系结构，并报告了一个广泛的实验评估系统，包括许多经典的例子，从逻辑编程终止文学和几个Prolog程序的体面的大小和复杂性。
2003-09-16 cs.PL
Ghost Signals: Verifying Termination of Busy-Waiting (Extended Version)
多处理器机器的程序通常执行忙等待同步。我们提出了第一个分离逻辑模块化验证终止的公平调度下，这样的程序。我们的逻辑要求证明作者将虚信号与每个忙等待循环相关联，并允许这样的循环在其相应的信号$s$未设置时停止。证明作者还必须对信号定义有根据的顺序，并证明如果循环线程持有设置信号$s^\prime$的义务，则$s^\prime$的顺序高于$s$。通过使用传统的共享状态不变量将重影信号的状态与数据结构的状态相关联，可以验证在任意数据结构上忙等待任意条件的程序。
2021-05-18 cs.LO cs.PL
The Probabilistic Termination Tool Amber
我们描述了琥珀工具证明和反驳终止一类概率的同时，程序与多项式算术，在一个完全自动化的方式。Amber将鞅理论与渐近边界函数的性质相结合，并实现了现有概率终止证明规则的放松版本，以证明/反驳概率循环的（正）几乎必然终止。Amber支持由符号常量参数化的程序，并从常见的概率分布中绘制。我们的实验比较给出了Amber优于现有最先进工具的实际证据。
2021-07-27 cs.PL
Type-Based Termination for Futures
本文将顺序语言中的大小类型终止性检查方法适配到并发场景，通过扩展半公理化相继式演算提出大小类型细化方案，借助无限宽有限深的类型推导树和新颖逻辑关系论证，实现基于futures的函数式并发程序的终止性验证。
2024-04-15 cs.LO cs.PL
Inference of termination conditions for numerical loops
本文提出了一种新的分析逻辑程序中数值计算终止性的方法。传统的方法由于整数的非良基性而无法对其进行分析。我们提出了一种技术，可以克服这些困难。我们的方法是基于转换程序的方式，允许集成和扩展技术最初开发的数值计算分析的框架中的查询映射对与知名的框架的可接受性。这样的整合不仅有助于理解终止行为的数值计算，但也允许自动执行正确的分析，这样的计算，从而扩展以前的工作基于约束的方法终止。在本文的最后一节中，我们讨论了可能的扩展技术，包括将一般的长期订单。
2001-06-26 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
Inference of termination conditions for numerical loops in Prolog
本文提出了一种新的分析逻辑程序中数值计算终止性的方法。传统的方法由于整数的非良基性而无法对其进行分析。我们提出了一种技术，可以克服这些困难。我们的方法是基于转换程序的方式，允许集成和扩展技术最初开发的数值计算分析的框架中的查询映射对与知名的框架的可接受性。这样的整合不仅有助于理解终止行为的数值计算，而且还允许我们自动执行正确的分析，这样的计算，通过扩展以前的工作基于约束的方法终止。最后，我们讨论了可能的扩展的技术，包括将一般术语排序。
2003-07-10 cs.LO cs.PL
A Productivity Checker for Logic Programming
递归推导的自动分析是逻辑程序设计中的一个难题。终结性和非终结性都是图灵完备语言中的不可判定问题。然而，一些声明性语言提供了一个实际的解决方案，通过明确区分程序是要被归纳还是共归纳地理解。对于要被归纳理解的程序，必须保证终止，而对于要被共归纳理解的程序，必须确保生产性非终止（或“生产力”）。在实践中，这种分类有助于更好地理解和实现一些非终止计算。逻辑编程是最早做出这种区分的声明性语言之一：在20世纪80年代，Lloyd和van Emden的"无限计算"捕获了推导的大步骤操作语义，产生无限项作为答案。在现代术语中，无穷大计算描述了逻辑编程中计算的“全局生产力”。大多数以共归纳为特征的程序设计语言也提供了一种观察性的或小步的生产力概念，作为全球生产力的计算对应物。这种生产力是通过检查无限计算的有限初始片段总是可以被观察到产生其无限答案项的有限部分来确保的。本文引入了逻辑程序的观测生产率概念，作为全局生产率的算法近似，给出了半判定观测生产率的有效方法，并给出了一个实现的逻辑程序的自动观测生产率检验器。
2016-08-19 cs.PL
Modular Verification for Almost-Sure Termination of Probabilistic Programs
在这项工作中，我们考虑几乎肯定终止问题的概率程序，询问是否一个给定的概率程序终止概率为1。可伸缩的程序分析方法通常依赖于模块化作为其理论基础。在非概率程序中，Floyd-霍尔逻辑的经典变式规则（V-规则）为模块化分析提供了基础。将该规则扩展到概率程序的几乎确定终止是相当棘手的，并且在[Fioriti and Hermanns 2015]中提出了一个概率变体。虽然所提出的概率变量谨慎地解决了可积性的关键问题，我们表明，所提出的模块化规则仍然是不健全的几乎肯定终止的概率程序。除了建立以前的规则的不健全，我们的贡献如下：首先，我们提出了一个健全的模块规则几乎确定终止的概率程序。我们的方法是基于一个新的概念下降上鞅。其次，对于算法方法，我们考虑下降上鞅是线性的，并表明它们可以在多项式时间合成。最后，我们提出了各种基准测试和几个自然的例子，模拟各种类型的嵌套而循环的概率程序的实验结果，并证明我们的方法是能够有效地证明其几乎肯定的终止属性。
2019-08-12 cs.LO cs.PL
On Lexicographic Proof Rules for Probabilistic Termination
我们认为几乎肯定（A. S.）概率程序的终止问题，它是经典命令式程序的随机扩展。字典序排序函数为非概率程序的终止提供了一种合理而实用的方法，并通过字典序排序上鞅（LexRSMs）将其扩展到概率程序.然而，在以前的工作中引入的LexRSM有一个限制，这阻碍了它们的自动化：它们的所有组件必须在所有可达状态中是非负的。这可能导致LexRSM不存在，即使是简单的终止程序。我们的贡献是双重的：首先，我们引入了一个广义的LexRSM允许某些组件是负的。非概率终止证明的这个标准特征迄今为止在概率环境中还不知道是合理的，因为合理性证明需要仔细分析潜在的随机过程。其次，我们提出了多项式时间算法，使用我们的广义LexRSM证明a.s.终止在广泛的线性算术程序类。
2021-08-04 cs.PL
Formalizing Termination Proofs under Polynomial Quasi-interpretations
函数式程序的终止性证明需要检查所有可能的归约路径。由于这种约简树的高度和大小之间的指数差距，没有朴素的形式化终止证明产生给定程序的多项式复杂度的连接。我们利用极小函数图的概念解决了这个问题，极小函数图是一个项及其范式的一组对，它被定义为单调算子的最小不动点。我们表明，终止证明的程序减少字典路径顺序（LPOs为短）和多项式准可解释的，可以最佳地进行在一个弱片段的Peano算法。这产生了另一种证明，即由LPO终止的多项式准可解释程序计算的每个函数在多项式空间中是可计算的。形式化确实是最优的，因为每个多项式空间可计算函数都可以由这样的程序计算。关键的观察是，在LPO终止程序下的最小函数图的归纳定义可以近似于沿着LPO的超限归纳。
2015-09-10 cs.CC cs.LO cs.PL
Termination Casts: A Flexible Approach to Termination with General Recursion
本文提出了一个类型和效果系统Teqt，它区分终止项和全函数与可能的发散项和部分函数，适用于具有一般递归和等式类型的λ演算.其中心思想是包含一个原始类型形式“Terminates t”，表示术语t是终止的;然后允许术语t被强制从可能发散到总和，使用Terminates t的证明。我们将这种递归函数称为终止类型转换，并展示如何使用它们实现终止递归。对于元理论的系统，我们描述了一个翻译从Teqt终止一般递归，简单类型的功能的逻辑理论。Teqt的每一个类型判断都被转化为一个定理，该定理表达了Teqt项的计算部分的适当终止性质。
2010-12-22 cs.PL
Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs
概率程序用实值随机变量和随机分支扩展了经典的命令式程序。这类程序最基本的活性属性是终止属性。定性（也称为几乎肯定）终止问题给出了一个概率程序，询问程序是否以概率1终止。虽然排序函数为非概率规划提供了一个合理而完整的方法，但将其扩展到概率规划是通过排序上鞅（RSM）实现的。虽然已经建立了深入的理论成果，他们的应用程序与非确定性的概率程序仅限于学术的例子。对于非概率程序，字典排序函数提供了一个组成和实际的方法，终止分析现实世界的程序。在这项工作中，我们介绍字典的RSM，并表明他们提出了一个健全的方法几乎肯定终止的概率程序与非确定性。我们表明，字典的RSM提供了一个工具，组合推理几乎肯定终止，和线性算术的概率程序，他们可以有效地合成（在多项式时间）。我们还表明，与其他限制，甚至可以通过字典的RSM得到预期的终止时间的渐近界。最后，我们提出的实验结果抽象的真实世界的程序来证明我们的方法的有效性。
2017-09-12 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
Stochastic Invariants for Probabilistic Termination
终止性是活性的基本性质之一，本文研究了实变量概率规划的终止性问题。以前的工作集中在定性问题，问是否输入程序终止概率~1（几乎肯定终止）。一个强有力的方法，这个定性问题的概念排名上鞅关于一组给定的不变量。定量问题（概率终止）要求终止概率的界限。现有的方法来解决概率终止的一个基本的和概念上的缺点是，即使上鞅考虑的概率行为的程序，获得的不变量完全忽略了概率方面。在这项工作中，我们解决的概率终止问题的线性算术概率程序的非确定性。我们定义了{ \em随机不变量}的概念，这是约束以及约束保持的概率界。引入了{ \em排斥上鞅}的概念。首先，我们证明了排斥上鞅可以用来获得随机不变量的概率上界。其次，我们从以下三个方面证明了排斥上鞅的有效性：（1）结合秩上鞅和排斥上鞅，我们可以计算终止概率的下界;（2）排斥上鞅为反驳几乎必然终止提供了证据;（3）结合秩上鞅和排斥上鞅，我们可以建立概率规划的持久性.我们还提出了相关的计算问题的结果和实验评估我们的方法在学术上的例子。
2016-11-16 cs.PL
Proving Non-termination by Program Reversal
提出了一种新的证明非确定整数规划非终止性的方法。我们的技术相当简单但有效。它依赖于一个纯粹的语法反转的程序的过渡系统，其次是一个基于约束的不变的合成与约束来自原始和反转的过渡系统。后一项任务是通过简单调用现成的SMT求解器来执行的，这使我们能够利用SMT求解的最新进展。此外，我们的方法提供了一个组合的功能不存在（作为一个整体）在以前的方法：它处理程序的非确定性，提供相对完整性的保证，并支持程序与多项式算术。与我们的原型工具RevTerm进行的实验表明，我们的方法，尽管它的简单性和更强的理论保证，是至少与国家的最先进的工具，往往实现了一个不平凡的改进下，其参数的适当配置。
2021-04-02 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
SM-based Semantics for Answer Set Programs Containing Conditional Literals and Arithmetic
University of Nebraska Omaha（内布拉斯加大学奥马哈分校）
本文基于 SM 算子为包含条件字面量与算术的答案集程序提出了一种无需接地的新语义，并证明了其与现有依赖无穷命题逻辑翻译的语义之间的精确对应关系。
2025-11-03 cs.AI cs.LO cs.PL
Automatic HFL(Z) Validity Checking for Program Verification
本文提出了一种自动化的方法来检验HFL（Z）公式的有效性，HFL（Z）是一种高阶逻辑，具有不动点算子和整数。结合Kobayashi et al.的减少，从高阶程序验证HFL（Z）的有效性检查，我们的方法产生一个全自动的，统一的验证方法的任意时间属性的高阶功能程序表示的模态μ演算，包括终止，非终止，公平终止，公平非终止，也分支时间属性。我们已经实现了我们的方法，并取得了可喜的实验结果。
2022-12-09 cs.PL
Evaluation of Logic Programs with Built-Ins and Aggregation: A Calculus for Bag Relations
我们提出了一个计划，用于翻译逻辑程序，这可能会使用聚合和算术，代数表达式表示袋关系的Herbrand宇宙的地面条款。为了评估这些关系的查询，我们开发了一个操作语义的基础上长期重写的代数表达式。这种方法可以利用算术恒等式并恢复一系列有用的策略，包括延迟工作直到它变得可能或必要的懒惰策略。
2020-10-20 cs.PL cs.SC
