LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:homework02 [2008/03/05 01:50]
david
sav08:homework02 [2008/03/05 16:05]
vkuncak
Line 92: Line 92:
  
 ===== Problem 5 (optional alternative to Problem 4) ===== ===== Problem 5 (optional alternative to Problem 4) =====
 +
 +(See also [[homework03]].)
  
 Extend the interpreter of Problem 3 with a verification-condition generator based on symbolic execution. ​ Verification condition generator should produce verification conditions where '​assume'​ becomes an assumption and where '​assert'​ becomes an assertion to be checked. ​ It should emit one verification condition for each '​assert'​. ​ It should also check that all loop invariants are preserved. ​ To prove the verification conditions, your verification-condition generator can feed them into the formDecider.opt prover from the [[:Jahob system]]. Extend the interpreter of Problem 3 with a verification-condition generator based on symbolic execution. ​ Verification condition generator should produce verification conditions where '​assume'​ becomes an assumption and where '​assert'​ becomes an assertion to be checked. ​ It should emit one verification condition for each '​assert'​. ​ It should also check that all loop invariants are preserved. ​ To prove the verification conditions, your verification-condition generator can feed them into the formDecider.opt prover from the [[:Jahob system]].