Exercises 03

Proof of

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

Next topics:

Some Project Suggestions

jahob system (and the PLDI 2008 paper)
theorem proving: decision procedures, interactive proof, couterexample search
checking programs in your favorite programming language by translation into existing verification systems
http://javapathfinder.sourceforge.net/
- On Delayed Choice Execution for Falsification
http://findbugs.sourceforge.net/ - extending a bug finding tool
coming up with new algorithms in the area of software analysis and verification (e.g. incremental algorithms, useful approximations for concurrency, heuristics, etc.)
decision procedures for e.g. linear arithmetic, constraints involving sets, etc.
program equivalence checking