# 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",
publisher = "Springer"
}