While termination checking tailored to real-world library code or frameworks has received ever-increasing attention during the last years, the complementary question of disproving termination properties as a means of debugging has largely been ignored so far. We present an approach to automatic non-termination checking that relates to termination checking in the same way as symbolic testing does to program verification. Our method is based on the automated generation of invariants that show that terminating states of a program are unreachable from certain initial states. Such initial states are identified using constraint-solving techniques. The method is fully implemented on top of a program verification system and available for download. We give an empirical evaluation of the approach using a collection of non-terminating example programs. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Velroyen, H., & Rümmer, P. (2008). Non-termination checking for imperative programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4966 LNCS, pp. 154–170). Springer Verlag. https://doi.org/10.1007/978-3-540-79124-9_11
Mendeley helps you to discover research relevant for your work.