LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
Last revision Both sides next revision
sav07_lecture_3_skeleton [2007/03/21 14:20]
vkuncak 		sav07_lecture_3_skeleton [2007/03/21 14:27]
vkuncak
Line 1: Line 1:
 ====== Lecture 3 (Skeleton) ====== ====== Lecture 3 (Skeleton) ======
  
-Recall ​what we are doing:+Summary of what we are doing:
  
 {{vcg-big-picture.png}} {{vcg-big-picture.png}}
  
  
-===== Converting ​programs ​(with simple values) to formulas ===== +===== Verification condition generation: converting ​programs ​into formulas =====
- +
  
 ==== Context ==== ==== Context ====
Line 164: Line 162:
  
  
-===== Proving quantifier-free linear arithmetic formulas =====+===== One useful decision procedure: ​Proving quantifier-free linear arithmetic formulas =====
  
 Suppose that we obtain (one or more) verification conditions of the form Suppose that we obtain (one or more) verification conditions of the form
Line 190: Line 188:
  
 Proof: small model theorem. Proof: small model theorem.
- 
- 
- 
- 
- 
- 
- 
- 
  
 ==== Small model theorem for Quantifier-Free Presburger Arithmetic (QFPA) ==== ==== Small model theorem for Quantifier-Free Presburger Arithmetic (QFPA) ====