LARA

Verifying Programs by Generating and Proving Formulas

Schema of a Simple Verifier Based on a Theorem Prover

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?