Differences

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

--- sav07_lecture_2 [2007/03/21 20:11]
vaibhav.rajan
+++ sav07_lecture_2 [2007/03/22 20:32]
vkuncak
@@ Line 505: / Line 505: @@
 Weakest preconditions of assignments make wp very appealing.
-===== Proving validity of linear arithmetic formulas =====
-Quantifier-Free Presburger arithmetic
-<latex>
-\begin{array}{l}
-\land, \lor, \lnot, \\
-x + y, K \cdot x, x < y, x=y
-\end{array}
-</latex>
-Validity versus satisfiability.  For all possible values of integers.
-Reduction to integer linear programming.
-Small model property.
-See, for example, {{papadimitriou81complexityintegerprogramming.pdf|paper by Papadimitriou}}.
-If we know more about the structure of solutions, we can take advantage of it as in
-{{seshiabryant04decidingquantifierfreepresburgerformulas.pdf|the paper by Seshia and Bryant}}.
@@ Line 582: / Line 555: @@
 left, right - uninterpreted functions (can have any value, depending on the program, unlike arithmetic functions such as +,-,* that have fixed interpretation).
-===== Reasoning about uninterpreted function symbols =====
-Essentially: quantifier-free first-order logic with equality.
-What are properties of equality?
-Congruence closure algorithm.  Here is {{nelsonoppen80decisionprocedurescongruenceclosure.pdf|the original paper by Nelson and Oppen}}.