Replication Package for Article: Termination Analysis without the Tears
Replication Package for Article: Termination Analysis without the Tears
复制标题
文章复制包：无泪终止分析
DOI：
10.1145/3410313
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Zachary Kincaid
中科院分区：
文献类型：
--
作者：
Shaowei Zhu;Zachary Kincaid
确定一个给定的程序是否终止是典型的不可判定问题。用于终止分析的算法可以分为两组：（1）具有在有限情况下工作的强行为保证的算法（例如，多面体环的线性排序函数的完全合成）;以及（2）广泛适用，但具有弱行为保证的算法（例如，终结者）。本文探讨了这两者之间的空间：我们如何设计实用的终止分析与有用的行为保证？本文提出了一种终止分析，它既是组合的（分析一个组合程序的结果是其组件的分析结果的函数）又是单调的（“更多的信息进入分析产生更多的信息出来”）。该文件有两个主要贡献。第一个是Tarjan的方法解决路径问题的图solveinfinitepath问题的扩展。这为构建成分终止分析提供了基础。第二个是基于这个框架的单调条件终止分析的集合。我们证明了我们的工具CompACT（条件终止的成分和可预测分析）与最先进的终止工具相比具有竞争力，同时提供更强的行为保证。
Determining whether a given program terminates is the quintessential undecidable problem. Algorithms for termination analysis may be classified 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), and (2) algorithms that are widely applicable, but have weak behavioral guarantees (e.g., Terminator). 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 bothcompositional(the result of analyzing a composite program is a function of the analysis results of its components) andmonotone(“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 solveinfinitepath 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.