Abstract
Invariants are a crucial component of the overall correctness of programs. We explore the theoretical limits for doing automatic invariant checking and show that invariant checking is decidable for a large class of programs that includes some recursive programs. The proof uses known results like the decidability of Presburger arithmetic and the semilinearity of the Parikh image of a regular language. Removing some of the restrictions on the program model leads to undecidability of the invariant checking problem. © 2009 Springer.
Cite
CITATION STYLE
Godoy, G., & Tiwari, A. (2009). Invariant checking for programs with procedure calls. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5673 LNCS, pp. 326–342). https://doi.org/10.1007/978-3-642-03237-0_22
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
