A Symbolic Simulation Approach to Assertional Program Verification

J. Matthews, J S. Moore, S. Ray, and

Draft, January 2005.

Abstract

We present a method for automating deductive proofs of machine-level sequential programs modeled using operational semantics. Given programs annotated by the user with assertions at cutpoints, we show how to use the operational semantics of the machine to automatically derive verification conditions by symbolic simulation. No verification condition generator is necessary, nor is it required to manually specify an inductive invariant for the machine model. Both partial and total correctness are considered. The methodology has been formalized in both the ACL2 and Isabelle theorem provers, and applied to verify programs on operational machine models in ACL2.

Relevant files