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:45] 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?200|Verifier Based on a Theorem Prover}} | + | {{sav08:theorem_prover2.jpg|Verifier Based on a Theorem Prover}} |
| ===== Steps in Verification ===== | ===== Steps in Verification ===== | ||
| - | * generate formulas representing program correctness | + | * 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 | ||