- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

sav08:homework02 [2008/03/05 01:50] david |
sav08:homework02 [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 86: | Line 86: | ||

constraint: F | constraint: F | ||

then the relation representing the meaning of $c$ should be given by the relation | then the relation representing the meaning of $c$ should be given by the relation | ||

- | \[ | + | \begin{equation*} |

\{("x" \rightarrow x0,"y" \rightarrow y0),("x" \rightarrow x,"y" \rightarrow y)) | x = e1 \land y = e2 \land F \} | \{("x" \rightarrow x0,"y" \rightarrow y0),("x" \rightarrow x,"y" \rightarrow y)) | x = e1 \land y = e2 \land F \} | ||

- | \] | + | \end{equation*} |

The final formula $F$ may or may not use additional existentially quantified variables. | The final formula $F$ may or may not use additional existentially quantified variables. | ||

===== 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]]. |