Lab for Automated Reasoning and Analysis LARA

Exercises 03

Proof of

\begin{equation*}
    S \setminus wp(r,Q) = sp(S \setminus Q,r^{-1})
\end{equation*}

Next topics:

  • generating formulas in Lecture 04
  • proving these formulas: SAT solvers, DPLL(T), resolution
  • inferring loop invariants
  • solving constraints derived from data-flow analysis

Some Project Suggestions

 
sav09/exercises_03.txt · Last modified: 2015/04/21 17:34 (external edit)
 
© EPFL 2018 - Legal notice