Disproving termination with overapproximation
Disproving termination with overapproximation
复制标题
DOI：
10.1109/fmcad.2014.6987597
复制
发表时间：
2014-10
期刊：
影响因子：
--
通讯作者：
B. Cook;Carsten Fuhs;K. Nimkar;P. O'Hearn
中科院分区：
文献类型：
--
作者：
B. Cook;Carsten Fuhs;K. Nimkar;P. O'Hearn
当使用已知技术（例如递归集）反驳终止时，过度近似程序转换关系的抽象是不合理的。在本文中，我们介绍了实时抽象，这是一种自然的抽象类，可以与最近的封闭递归集概念相结合，以彻底反驳终止。为了证明这种新方法的实际用途，我们展示了如何使用线性过近似来显示具有非线性、不确定性和基于堆的命令的程序。
When disproving termination using known techniques (e.g. recurrence sets), abstractions that overapproximate the program's transition relation are unsound. In this paper we introduce live abstractions, a natural class of abstractions that can be combined with the recent concept of closed recurrence sets to soundly disprove termination. To demonstrate the practical usefulness of this new approach we show how programs with nonlinear, nondeterministic, and heap-based commands can be shown nonterminating using linear overapproximations.