A Mechanical Analysis of Program Verification Strategies
S. Ray, W. A. Hunt, Jr., J. Matthews, and J S. Moore
To Appear in Journal of
Automated Reasoning. Springer.
© 2008 Springer. The original
publication is available at www.springerlink.com.
Abstract
We analyze three proof strategies commonly used in deductive
verification of deterministic sequential programs formalized with
operational semantics. The strategies are: (i) stepwise invariants, (ii) clock functions, and (iii) inductive assertions. We show how
to formalize the strategies in the logic of the ACL2 theorem prover.
Based on our formalization, we prove that each strategy is both sound and complete. The completeness result implies that given
any proof of correctness of a sequential program one can derive a
proof in each of the above strategies. The soundness and completeness
theorems have been mechanically checked with ACL2.
Relevant files