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
Next revision Both sides next revision
sav07_lecture_3_skeleton [2007/03/21 12:28]
vkuncak 		sav07_lecture_3_skeleton [2007/03/21 14:26]
vkuncak
Line 1: Line 1:
 ====== Lecture 3 (Skeleton) ====== ====== Lecture 3 (Skeleton) ======
  
-===== Converting programs (with simple values) to formulas =====+Recall what we are doing:
  
 +{{vcg-big-picture.png}}
  
 +
 +===== Verification condition generation: converting programs into formulas =====
  
 ==== Context ==== ==== Context ====
Line 158: Line 161:
  
  
-===== 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 165: Line 169:
 \end{equation*} \end{equation*}
  
-whose validity we need to prove. ​ We here assume that F contains only  +whose validity we need to prove. ​ We here assume that F contains only linear arithmetic.  ​Note: we can check satisfiability of $F\ \land\ (\mbox{error}=\mbox{true})$.  We show an algorithm to check this satisfiability.
- +
-Note: we can check satisfiability of $F\ \land\ (\mbox{error}=\mbox{true})$.+
  
 ==== Quantifier Presburger arithmetic ==== ==== Quantifier Presburger arithmetic ====
Line 186: 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) ====