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?