Time |
Topic |
| 10.00 - 10.30 | Welcome coffee |
| 10.30 - 10.50 | Welcome |
| 10.50 - 11.50 | Verification of real-world C programs with
VCC (Invited Talk) Stephan Tobies |
| 11.50 - 12.10 | Sum comprehensions in KeY Christian Engel |
| 12.10 - 12.30 | Integration of external SMT solvers Simon Greiner |
| 12.30 - 14.00 | Lunch |
| 14.00 - 14.30 | Abstract Object Creation in Dynamic Logic Wolfgang Ahrendt |
| 14.30 - 15.00 | A program logic combining partial evaluation and symbolic execution Reiner Hähnle / Richard Bubel |
| 15.00 - 15.30 | Observer symbols Mattias Ulbrich / Benjamin Weiß |
| 15.30 - 16.00 | Coffee break |
| 16.00 - 16.30 | A Calculus for Data Abstraction Roman Krenický |
| 16.30 - 17.00 | An Explicit Heap in Java DL Peter H. Schmitt / Benjamin Weiß |
| 17.00 - 18.00 | Discussion: The present state of
the KeY project and its future course Introduction and moderation: Peter H. Schmitt |
Time |
Topic |
| 09.00 - 10.00 | Proofs and Counterexamples for Java Programs (Invited Talk) Viktor Kuncak |
| 10.00 - 10.30 | Bounded Model Checking of C programs Carsten Sinz |
| 10.30 - 11.00 | Coffee break |
| 11.00 - 11.30 | On the relation of BDD based and resolution based proof systems Olga Tveretina |
| 11.30 - 12.00 | The Verisoft XT Project Avionics Thorsten Bormer |
| 12.00 - 12.30 | On the generation of test cases for embedded software in Avionics Philipp Rümmer |
| 12.30 - 13.30 | Lunch |
| 13.30 - 14.30 | Guided tour through the cathedral |
| 15.00 - 15.30 | Verification in Sensor Networks Frank Werner |
| 15.30 - 16.00 | Formal Semantics for JML Daniel Bruns |
| 16.00 - 16.30 | Midlet Navigation Graphs in JML Wojciech Mostowski |
| 16.30 - 17.00 | Coffee break |
| 17.00 - 17.30 | Adapting KeY for the Creol Modelling Language Maximilian Dylla |
| 17.30 - 18.00 | KeYmaera - Verifying Hybrid Systems in KeY Jan-David Quesel |
| 18.00 - 18.30 | The Proof Assistant PAF! Séverine Maingaud |
Time |
Topic |
| 09.00 - 09.30 | Bit-vector extensions for KeY Olivier Borne |
| 09.30 - 10.00 | A First-Order Logic with First-Class Types Michael Walter |
| 10.00 - 10.30 | Finding bugs from failed verification attempts Christoph Gladisch |
| 10.30 - 11.00 | Coffee break |
| 11.00 - 11.20 | Test Generation in the Model Checking field David Faragó |
| 11.20 - 11.30 | The Charter project Wolfgang Ahrendt |
| 11.30 - 12.30 | Discussion: Strategy engine design
and parallel proving Introduction: Jan-David Quesel |
| 12.30 - 14.00 | Lunch |