# 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?