Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
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
 
© EPFL 2018 - Legal notice