Program
| 9.00 | Yannick Moy |
|---|---|
| Union and Cast in Deductive Verification
[paper, slides] | |
| 9.30 | Matthias Daum |
| Reasoning on Data-Parallel Programs in
Isabelle/Hol
[paper, slides] | |
| 10.00 | Christoph D. Gladisch |
|
How C
differs from Java for Symbolic Program Execution
[paper, slides] |
| 10.30 - 11.15 Coffee |
|---|
| 11.15 | Sandrine Blazy |
|---|---|
| Experiments in validating formal semantics for C | |
| 11.45 | Oleg Mürk, Daniel Larsson, Reiner Hähnle |
| A Dynamic Logic for Deductive Verification of C Programs with KeY-C | |
| 12.15 | Hendrik Tews |
| Formal Methods in the Robin project: Specification and verification of the Nova microhypervisor |
| 12.45 - 13.45 Lunch |
|---|
| 13.45 | Ansgar Fehnker, Ralf Huuck, Felix Rauch, Sean Seefried |
|---|---|
| Analysing Embedded System Software | |
| 14.15 | Roberto Bagnara, Patricia M. Hill, Andrea Pescetti, Enea Zaffanella |
| Verification of C Programs Via Natural Semantics and Abstract Interpretation | |
| 14.45 | Taras Glek |
|
DeHydra Source Analysis Tool
[paper, slides, slides.tar.gz] | |
| 15.15 - 15.45 Tea |
|---|
| 15.45 | Wolfram Schulte, Jan Smans, Songtao Xia |
|---|---|
| A Glimpse of a
Verifying C Compiler
[paper, slides] | |
| 16.15 | Hendrik Tews |
| Olmar: manipulating C and C++ abstract syntax trees in Ocaml | |
| 16.45 | Final Discussion |
Last updated: June 26.