Invariant Checking for Programs with Procedure Calls

Citation

Godoy, G., Tiwari, A. (2009). Invariant Checking for Programs with Procedure Calls. In: Palsberg, J., Su, Z. (eds) Static Analysis. SAS 2009. Lecture Notes in Computer Science, vol 5673. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03237-0_22

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.

Keywords: Program Model, Basic Block, Regular Language, Procedure Call, Recursive Program

↓ View online

Read more from SRI

  • A photo of Mary Wagner

    Recognizing the life and work of Mary Wagner 

    A cherished SRI colleague and globally respected leader in education research, Mary Wagner leaves behind an extraordinary legacy of groundbreaking work supporting children and youth with disabilities and their families.

  • Testing XRGo in a robotics laboratory

    Robots in the cleanroom

    A global health leader is exploring how SRI’s robotic telemanipulation technology can enhance pharmaceutical manufacturing.

  • SRI research aims to make generative AI more trustworthy

    Researchers have developed a new framework that reduces generative AI hallucinations by up to 32%.