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] (current) 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 |