- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

sav07_homework_2 [2007/03/30 13:58] vkuncak |
sav07_homework_2 [2007/04/06 20:15] (current) vkuncak |
||
---|---|---|---|

Line 1: | Line 1: | ||

====== Homework 2 ====== | ====== Homework 2 ====== | ||

+ | |||

Line 10: | Line 11: | ||

F ::= A | (F&F) | (F|F) | ~F | ALL v.F | EX v.F | F ::= A | (F&F) | (F|F) | ~F | ALL v.F | EX v.F | ||

- | A ::= v=v | v + K <= v | + | A ::= v=v | v + K ≤ v |

K ::= ... -2 | -1 | 0 | 1 | 2 | ... | K ::= ... -2 | -1 | 0 | 1 | 2 | ... | ||

v ::= x | y | z | ... | v ::= x | y | z | ... | ||

Line 25: | Line 26: | ||

**Hint**: You should be able to reduce the problem to reasoning about conjunctions and generate a disjunction over total orders over terms of form v+c. Alternatively, you may be able to use some ideas of [[http://citeseer.ist.psu.edu/71579.html|Fourier-Motzkin elimination]], but it is not necessary for this problem to have an efficient algorithm, only an algorithm that works in principle. | **Hint**: You should be able to reduce the problem to reasoning about conjunctions and generate a disjunction over total orders over terms of form v+c. Alternatively, you may be able to use some ideas of [[http://citeseer.ist.psu.edu/71579.html|Fourier-Motzkin elimination]], but it is not necessary for this problem to have an efficient algorithm, only an algorithm that works in principle. | ||

- | |||

- | |||

- | |||

==== Verification condition generator ==== | ==== Verification condition generator ==== |