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

  • surgeons around a surgical robot

    The SRI research behind today’s surgical robotics

    Intuitive’s da Vinci 5 system represents a major leap in robotic-assisted medicine. It all started at SRI, which continues to advance teleoperation technologies.

  • a collage of digital graphs

    A banner year for quantum

    SRI-managed QED-C’s annual report on quantum trends captures an industry accelerating rapidly from technical promise toward major global impact.

  • ICE Cube containing SRI’s aerogel experiment, photographed prior to launch. Source: Aerospace Applications North America

    An SRI carbon capture experiment launches into space

    By synthesizing carbon-absorbing aerogels in microgravity, SRI research will give us a rare glimpse into how these materials could be radically improved.