LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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