Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
sav08:big_picture_of_vcg [2009/02/22 16:44] vkuncak |
sav08:big_picture_of_vcg [2009/02/22 16:45] 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 === | + | ===== Steps in Verification ===== |
| * generate formulas representing program correctness | * generate formulas representing program correctness | ||
| Line 15: | Line 15: | ||
| * 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 21: | ||
| * 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? | ||