A Mechanical Analysis of Program Verification Strategies

S. Ray, W. A. Hunt, Jr., J. Matthews, and J S. Moore

Journal of Automated Reasoning, volume 40(4), May 2008, pages 245-269. 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

Paper (ps, pdf, Online Version from Springer )

Supporting ACL2 proof scripts: See the directory books/proofstyles/ in the current ACL2 distribution.

BibTex

@Article{ray-mechanical,
  author    = "S. Ray and Hunt, Jr., W. A. and J. Matthews and J S. Moore",
  title     = "{A Mechanical Analysis of Program Verification Strategies}",
  journal   = "{Journal of Automated Reasoning}",
  volume    = "40",
  number    = "4",
  pages     = "245-269",
  publisher = "{Springer}",
  month     = may,
  year      = "2008"
}