Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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 ====
 
sav07_homework_2.txt · Last modified: 2007/04/06 20:15 by vkuncak