Abstract
In this talk I will describe new tools that allow us to automatically prove termination and other liveness properties of software systems. In particular I will discuss the Terminator program termination prover and its application to the problem of showing that Windows device driver event-handling routines always eventually stop responding to events.
Chapter PDF
Similar content being viewed by others
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cook, B. (2007). Automatically Proving Program Termination. In: Damm, W., Hermanns, H. (eds) Computer Aided Verification. CAV 2007. Lecture Notes in Computer Science, vol 4590. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73368-3_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-73368-3_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73367-6
Online ISBN: 978-3-540-73368-3
eBook Packages: Computer ScienceComputer Science (R0)