C/C++ Verification Workshop, July 2

colocated with IFM 2007 in Oxford, UK (July 2-7)


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.