Abstract
Because the halting problem is undecidable, many have considered the dream of automatically proving termination (and other liveness properties) to be impossible. While not refuting Turing’s original result of undecidability, recent research now makes this dream a practical reality. I will describe this recent work and its application to industrial software and models of biological systems. I will also describe recent adaptations of these new technologies to the problem of proving temporal properties in logics such as CTL and LTL.
Chapter PDF
Similar content being viewed by others
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cook, B. (2011). Advances in Proving Program Termination and Liveness. In: Bjørner, N., Sofronie-Stokkermans, V. (eds) Automated Deduction – CADE-23. CADE 2011. Lecture Notes in Computer Science(), vol 6803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22438-6_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-22438-6_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22437-9
Online ISBN: 978-3-642-22438-6
eBook Packages: Computer ScienceComputer Science (R0)