Proving non-termination

9 years 2 months ago
Proving non-termination
The search for proof and the search for counterexamples (bugs) are complementary activities that need to be pursued concurrently in order to maximize the practical success rate of verification tools. While this is well-understood in safety verification, in liveness verification the focus, to date, has been almost exclusively on the search for termination proofs. A counterexample to termination is an infinite, nonterminating program execution. In this paper, we search for such counterexamples. The search proceeds in two phases, by first dynamically enumerating lasso-shaped candidate paths for counterexamples, and then statically proving their feasibility. We illustrate the utility of our nontermination prover, TNT, on several nontrivial examples, some of which require bit-level reasoning about integer representations. Categories and Subject Descriptors D.2.4 [Software]: Software Engineering--Program Verification; D.4.5 [Software]: Operating Systems--Reliability General Terms Reliabilit...
Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumda
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where POPL
Authors Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, Ru-Gang Xu
Comments (0)