Verification Condition Generation via Theorem Proving

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

In M. Hermann and A. Voronkov, editors, Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2006), Phnom Penh, Cambodia, November 2006, volume 4246 of LNCS, pages 362-376. Springer-Verlag

© Springer-Verlag Berlin Heidelberg 2006.

Abstract

We present a method to convert (i) an operational semantics for a given machine language, and (ii) an off-the-shelf theorem prover, into a high assurance verification condition generator (VCG). Given a program annotated with assertions at cutpoints, we show how to use the theorem prover directly on the operational semantics to generate verification conditions analogous to those produced by a custom-built VCG. Thus no separate VCG is necessary, and the theorem prover can be employed both to generate and to discharge the verification conditions. The method handles both partial and total correctness. It is also compositional in that the correctness of a subroutine needs to be proved once, rather than at each call site. The method has been used to verify several machine-level programs using the ACL2 theorem prover.

Relevant files

Paper (ps, pdf)
Slides (ppt, pdf)
[Note: The original slides were created in powerpoint with audio at the request of the LPAR 2006 organizers, since I could not attend the conference personally. Unfortunately, it was later determined that they could not permit an audio-visual presentation; so the slides were never presented. I have put them up here in the hope that they might provide a better explanation of the material. However, I removed the audio from the powerpoint to facilitate download.]

BibTex

@Inproceedings{matthews-verification,
 author       = "J. Matthews and J S. Moore and S. Ray and D. Vroon",
 title        = "{Verification Condition Generation Via Theorem Proving}",
 booktitle    = "{Proceedings of the $13$th International Conference on 
                  Logic for Programming, Artificial Intelligence, and 
                  Reasoning (LPAR 2006)}",
 editor       = "M. Hermann and A. Voronkov",
 month        = nov,
 year         = "2006",
 series       = "LNCS",
 address      = "{Phnom Penh, Cambodia}",
 volume       = "4246",
 pages        = "362-376"
}