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
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 in today'​s class:
  
 {{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) ====