A MECHANICALLY VERIFIED VERIFICATION CONDITION GENERATOR

Verification Condition Generator (VCG) tools have been effective in si mplifying the task of proving programs correct. However, in the past t hese VCG tools have in general not themselves been mechanically proven , so any proof using and depending on these VCGs might not be sound, I n our work, we define and rigorously prove correct a VCG tool within t he HOL theorem proving system, for a standard while-loop language, wit h one new feature not usually treated: expressions with side effects. Starting from a structural operational semantics of this programming l anguage, we prove as theorems the axioms and rules of inference of a H oare-style axiomatic semantics, verifying their soundness. This axioma tic semantics is then used to define and prove correct a VCG tool for this language. Finally, this verified VCG is applied to an example pro gram to verify its correctness.