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.
翻译:确定某个程序终止是否为典型的不可量化问题。 用于终止分析的算法分为两类:(1) 具有在有限情况下起作用的强力行为保障的算法( 例如, 多元环( Podelski 和 Rybalchenko, 2004) 的线性排序功能的完整合成),(2) 广泛适用但行为保障薄弱的算法( 例如, 终结者 [ Cook 等人, 2006] ) 。 本文调查了以下两者之间的空间: 我们如何设计实用的终止分析器, 提供有用的行为保障? 本文展示了终止分析器的终止分析器, 其构成性分析的结果是其组成部分分析结果的函数) 和单体( 分析器中的更多信息产生更多信息 ) 。 该文件有两大关键贡献。 首先是扩展了Tarjan在图表中解决路径问题的方法, 以解决无限路径问题。 这为构建终止分析提供了基础。 第二是基于这一框架的单项有条件终止分析器分析器( 提供更强的终止性分析工具, 我们展示了更强的终止性分析工具。