Abstract
We show how the problem of nontermination proving can be reduced to a question of underapproximation search guided by a safety prover. This reduction leads to new nontermination proving implementation strategies based on existing tools for safety proving. Our preliminary implementation beats existing tools. Furthermore, our approach leads to easy support for programs with unbounded nondeterminism. © 2014 Springer-Verlag.
Cite
CITATION STYLE
Chen, H. Y., Cook, B., Fuhs, C., Nimkar, K., & O’Hearn, P. (2014). Proving nontermination via safety. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8413 LNCS, pp. 156–171). Springer Verlag. https://doi.org/10.1007/978-3-642-54862-8_11
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
