ProjectsToDo

Research (mini-)projects you plan to do

Koen (with Chris Lynch from Potsdam): Ordered resolution and instance-based theorem proving
Koen+Niklas: A SAT-based model checker that will perform well in next year's Model checking competition
Koen+Niklas: Re-engineer Paradox, so that it will win the CASC competition next year (again)
Koen+Niklas: Improve Equinox so that it does OK in next year's CASC
Koen (with Christoph Weidenbach from MPI): Investigate "safety property checking by model finding" technique. Applications: (1) solve Christoph's problems using Paradox, (2) solve SMT problems (with arrays) using Paradox, (3) model information flow in a web-browser and prove correctness (possibly with some security person)