Towards Structured Proofs for Program Verification (Ongoing Work)

ABSTRACT. The first step in program verification is often a call to a verification condition generator (VCG) which decomposes a program into a set of logical formulas, the verification conditions. These verification conditions must then be discharged manually.

The process of constructing the verification conditions loses much of the structure of the original program. In this article, we extend the VCG to attach annotations to the verification conditions and hence preserve the program structure. We implemented this approach in the Isabelle theorem prover. This allows us to replace unstructured proof scripts by structured Isar proofs.