Verifying Programs by Generating and Proving Formulas
Schema of a Simple Verifier Based on a Theorem Prover
Steps in Verification
- generate formulas implying program correctness
- attempt to prove formulas
- if formula is true, program is correct
- if formula has a counterexample, it indicates one of these:
- error in the program
- error in the property
- error in auxiliary statements (e.g. loop invariants)
Terminology
- generated formulas: verification conditions
- generation process: verification-condition generation
- program generating formulas: verification-condition generator (VCG)
Questions Remaining
How do we compute verification conditions?
To answer this, we ask: how do we assign mathematical meaning to programs?