Termination and non-termination specification inference
Termination and non-termination specification inference
复制标题
DOI：
10.1145/2737924.2737993
复制
发表时间：
2015-06
期刊：
影响因子：
--
通讯作者：
T. Le;S. Qin;W. Chin
中科院分区：
文献类型：
--
作者：
T. Le;S. Qin;W. Chin
证明命令式程序可终止性和不可终止性的技术通常被认为是正交机制。在本文中，我们提出了一种新的机制，分析和证明程序终止和非终止在同一时间。我们首先引入了二阶终止约束的概念，并通过Hoare式验证积累了一组关系假设。然后，我们解决这些假设与案例分析，以确定（条件）终止和非终止的情况下表示的一些规格说明逻辑形式。与目前的方法相比，我们的技术可以为每个方法构建终止和非终止行为的摘要。这使得模块化和重用我们的终止和非终止证明过程。我们已经测试了我们的工具，从最近的终止竞争的样本程序，并与最先进的终止分析器相比，毫不逊色。
Techniques for proving termination and non-termination of imperative programs are usually considered as orthogonal mechanisms. In this paper, we propose a novel mechanism that analyzes and proves both program termination and non-termination at the same time. We first introduce the concept of second-order termination constraints and accumulate a set of relational assumptions on them via a Hoare-style verification. We then solve these assumptions with case analysis to determine the (conditional) termination and non- termination scenarios expressed in some specification logic form. In contrast to current approaches, our technique can construct a summary of terminating and non-terminating behaviors for each method. This enables modularity and reuse for our termination and non-termination proving processes. We have tested our tool on sample programs from a recent termination competition, and compared favorably against state-of-the-art termination analyzers.