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 09:37]
vkuncak 		sav07_lecture_3_skeleton [2007/03/21 10:41]
vkuncak
Line 127: Line 127:
 Alternative:​ Alternative:​
   * decide that you will only loop for formulas of restricted form, as in abstract interpretation and data flow analysis (next week)   * decide that you will only loop for formulas of restricted form, as in abstract interpretation and data flow analysis (next week)
 +
  
  
Line 132: Line 133:
  
 Suppose that we obtain (one or more) verification conditions of the form Suppose that we obtain (one or more) verification conditions of the form
 +\begin{equation*}
 + F \rightarrow \mbox{error}=\mbox{false}
 +\end{equation*}
 +
 +whose validity we need to prove. ​ We here assume that F contains only 
 +
 +Note: we can check satisfiability of $F \land \mbox{error}=\mbox{true}$.
  
 ==== Quantifier Presburger arithmetic ==== ==== Quantifier Presburger arithmetic ====
Line 151: Line 159:
 Proof: small model theorem. Proof: small model theorem.
  
-==== Small model theorem for quantifier-free Presburger ​arithmetic ​====+ 
 + 
 + 
 + 
 + 
 + 
 + 
 +==== Small model theorem for Quantifier-Free Presburger ​Arithmetic (QFPA) ​====
  
 First step: transform to disjunctive normal form. First step: transform to disjunctive normal form.
Line 157: Line 172:
 Next: reduce to integer linear programming:​ Next: reduce to integer linear programming:​
 \begin{equation*} \begin{equation*}
-  ​Ax = b, x \geq 0+  ​A\vec x = \vec b, \qquad \vec x \geq \vec 0
 \end{equation*} \end{equation*}
 where $A \in {\cal Z}^{m,n}$ and $x \in {\cal Z}^n$. where $A \in {\cal Z}^{m,n}$ and $x \in {\cal Z}^n$.
  
-Then use small model theorem for integer linear programming.+Then solve integer linear programming ​(ILP) problem 
 +  * [[wk>​Integer Linear Programming]] 
 +  * online book chapter on ILP 
 +  * [[http://​www.gnu.org/​software/​glpk/​|GLPK]] tool
  
-Short proof by +We can prove small model theorem for ILP - gives bound on search. 
 + 
 +Short proof by {{papadimitriou81complexityintegerprogramming.pdf|Papadimitriou}}:​ 
 +  * solution of Ax=b (A regular) has as components rationals of form p/q with bounded p,q 
 +  * duality of linear programming 
 +  * obtains bound $M = n(ma)^{2m+1}$,​ which needs $(2m+1)(\log n + \log m + \log a)$ bits 
 +  * we could encode the problem into SAT: use circuits for addition, comparison etc. 
 + 
 +Note: if small model theorem applies to conjunctions,​ it also applies to arbitrary QFPA formulas. ​  
 + 
 +Moreover, one can improve these bounds. ​ One tool based on these ideas is [[http://​www.cs.cmu.edu/​~uclid/​|UCLID]]. 
 + 
 +Alternative:​ enumerate disjuncts of DNF on demand, each disjunct is a conjunction,​ then use ILP techniques (often first solve the underlying linear programming problem over reals). ​ Many SMT tools are based on this idea (along with Nelson-Oppen combination:​ next class). 
 +  * [[http://​www.cs.nyu.edu/​acsys/​cvc3/​download.html|CVC3]] (successor of CVC Lite) 
 +  * [[http://​combination.cs.uiowa.edu/​smtlib/​|SMT-LIB]] Standard for formulas, competition
  
-Tools: 
-  * [[http://​www.cs.cmu.edu/​~uclid/​|UCLID]] 
  
 ==== Full Presburger arithmetic ==== ==== Full Presburger arithmetic ====
  
 Full Presburger arithmetic is also decidable. Full Presburger arithmetic is also decidable.
 +
 +Approaches:
 +  * Quantifier-Elimination (Omega tool from Maryland) - see homework
 +  * Automata Theoretic approaches: LASH, MONA (as a special case)
  
 ===== Papers ===== ===== Papers =====