====== Verifying Programs by Generating and Proving Formulas ======

===== Schema of a Simple Verifier Based on a Theorem Prover =====

{{sav08:theorem_prover2.jpg|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?