Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:big_picture_of_vcg [2009/02/22 16:44] vkuncak |
sav08:big_picture_of_vcg [2010/03/02 14:29] vkuncak |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| ===== Schema of a Simple Verifier Based on a Theorem Prover ===== | ===== Schema of a Simple Verifier Based on a Theorem Prover ===== | ||
| - | {{sav08:theorem_prover2.jpg|}} | + | {{sav08:theorem_prover2.jpg|Verifier Based on a Theorem Prover}} |
| - | === Steps in Verification === | ||
| - | * generate formulas representing program correctness | + | ===== Steps in Verification ===== |
| + | |||
| + | * generate formulas implying program correctness | ||
| * attempt to prove formulas | * attempt to prove formulas | ||
| * if formula is true, program is correct | * if formula is true, program is correct | ||
| Line 15: | Line 16: | ||
| * error in auxiliary statements (e.g. loop invariants) | * error in auxiliary statements (e.g. loop invariants) | ||
| - | === Terminology === | + | ===== Terminology ===== |
| * generated formulas: //verification conditions// | * generated formulas: //verification conditions// | ||
| Line 21: | Line 22: | ||
| * program generating formulas: //verification-condition generator// (VCG) | * program generating formulas: //verification-condition generator// (VCG) | ||
| - | === Questions Remaining === | + | ===== Questions Remaining ===== |
| How do we compute verification conditions? | How do we compute verification conditions? | ||