Abstract
Originally, the concepts of transition invariants and transition predicate abstraction were used to formulate a proof rule and an abstraction-based algorithm for the verification of liveness properties of concurrent programs under fairness assumptions. This note applies the two concepts for proving termination of sequential programs. We believe that the specialized setting exhibits the underlying principles in a more direct way.
Chapter PDF
Similar content being viewed by others
References
Podelski, A., Rybalchenko, A.: Software model checking of liveness properties via transition invariants. Technical Report MPI-I-2003-2-004, Max-Planck-Institut für Informatik (December 2003), http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2003-2-004
Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004)
Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS 2004: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, Washington, DC, USA, pp. 32–41. IEEE Computer Society Press, Los Alamitos (2004)
Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: POPL 2005: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, vol. 32, pp. 132–144. ACM, New York (2005)
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
Podelski, A., Rybalchenko, A. (2011). Transition Invariants and Transition Predicate Abstraction for Program Termination. In: Abdulla, P.A., Leino, K.R.M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2011. Lecture Notes in Computer Science, vol 6605. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19835-9_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-19835-9_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19834-2
Online ISBN: 978-3-642-19835-9
eBook Packages: Computer ScienceComputer Science (R0)