Stephan Tobies |
Verification of real-world C programs with VCC (Invited Talk) |
| Christian Engel |
Sum comprehensions in KeY |
| Simon Greiner |
Integration of external SMT solvers |
| Wolfgang Ahrendt |
Abstract Object Creation in Dynamic Logic |
| Reiner Hähnle / Richard Bubel |
A program logic combining partial evaluation and symbolic execution |
| Mattias Ulbrich / Benjamin Weiß |
Observer symbols |
| Roman Krenický |
A Calculus for Data Abstraction |
| Peter H. Schmitt / Benjamin Weiß |
An Explicit Heap in Java
DL |
| Viktor Kuncak |
Proofs and Counterexamples for Java Programs (Invited Talk) |
| Carsten Sinz |
Bounded Model Checking of C programs |
| Thorsten Bormer |
Verification of System Calls in PikeOS |
| Philipp Rümmer |
On the generation of test cases for embedded software in Avionics |
| Frank Werner |
Verification in Sensor Networks |
| Daniel Bruns |
Formal Semantics for JML |
| Wojciech Mostowski |
Midlet Navigation Graphs in JML |
| Maximilian Dylla |
Adapting KeY for the Creol Modelling Language |
| Jan-David Quesel |
KeYmaera - Verifying Hybrid Systems in KeY |
| Séverine Maingaud |
The Proof Assistant PAF! |
Olivier Borne |
Bit-vector extensions for KeY
[also as PDF] |
| Michael Walter |
A First-Order Logic with First-Class Types |
| Christoph Gladisch |
Finding bugs from failed verification attempts |
