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 12:28]
vkuncak 		sav07_lecture_3_skeleton [2007/03/21 14:27]
vkuncak
Line 1: Line 1:
 ====== Lecture 3 (Skeleton) ====== ====== Lecture 3 (Skeleton) ======
  
-===== Converting programs (with simple values) to formulas =====+Summary of what we are doing in today'​s class:
  
 +{{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) ====