没有眼泪的终止分析
Termination Analysis Without the Tears
摘要：
确定一个给定的程序是否终止是典型的不可判定问题。终止分析的算法分为两组：（1）具有强行为保证的算法，在有限的情况下工作（例如，多面体环的线性排序函数的完全综合[Podelski和Rybalchenko，2004]），以及（2）广泛适用，但具有弱行为保证的算法（例如，终结者[Cook等人，2006]）。本文探讨了这两者之间的空间：我们如何设计实用的终止分析与有用的行为保证？本文提出了一种终止分析，这是组合（分析一个复合程序的结果是其组件的分析结果的函数）和单调（“更多的信息进入分析产生更多的信息”）。该文件有两个主要贡献。第一个是一个扩展的Tarjan的方法解决路径问题的图解决无限路径问题。这为构建成分终止分析提供了基础。第二个是基于这个框架的单调条件终止分析的集合。我们证明了我们的工具CompACT（条件终止的成分和可预测分析）与最先进的终止工具相比具有竞争力，同时提供更强的行为保证。
英文摘要：
Determining whether a given program terminates is the quintessential undecidable problem. Algorithms for termination analysis are divided into two groups: (1) algorithms with strong behavioral guarantees that work in limited circumstances (e.g., complete synthesis of linear ranking functions for polyhedral loops [Podelski and Rybalchenko, 2004]), and (2) algorithms that are widely applicable, but have weak behavioral guarantees (e.g., Terminator [Cook et al., 2006]). This paper investigates the space in between: how can we design practical termination analyzers with useful behavioral guarantees? This paper presents a termination analysis that is both compositional (the result of analyzing a composite program is a function of the analysis results of its components) and monotone ("more information into the analysis yields more information out"). The paper has two key contributions. The first is an extension of Tarjan's method for solving path problems in graphs to solve infinite path problems. This provides a foundation upon which to build compositional termination analyses. The second is a collection of monotone conditional termination analyses based on this framework. We demonstrate that our tool ComPACT (Compositional and Predictable Analysis for Conditional Termination) is competitive with state-of-the-art termination tools while providing stronger behavioral guarantees.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
