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_3_skeleton [2007/03/21 09:48] vkuncak |
sav07_lecture_3_skeleton [2007/03/21 09:51] vkuncak |
||
|---|---|---|---|
| Line 172: | Line 172: | ||
| * [[http://www.cs.nyu.edu/acsys/cvc3/download.html|CVC3]] (successor of CVC Lite) | * [[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 | * [[http://combination.cs.uiowa.edu/smtlib/|SMT-LIB]] Standard for formulas, competition | ||
| + | |||
| ==== 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 ===== | ||