Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav07_lecture_2 [2007/03/22 20:30] vkuncak |
sav07_lecture_2 [2007/03/22 20:32] vkuncak |
||
|---|---|---|---|
| Line 505: | Line 505: | ||
| Weakest preconditions of assignments make wp very appealing. | 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}}. | ||
| - | |||