Differences
This shows you the differences between two versions of the page.
Both sides previous 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 4: | Line 4: | ||
{{sav08:theorem_prover2.jpg|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 |