Program

[The titles link to the respective abstracts; there, you can also download the papers.
The complete workshop proceedings are also available.]

Friday, 26 August

9:00 - 10:00 Invited Talk
Refinement-based CFG Reconstruction from Executable Files
Sebastien Bardin (CEA)
10:00 - 10:15 Coffee Break
10:15 - 11:15 Session I
Adaptable Value-Set Analysis for Low-Level Code
Jörg Brauer, Rene Rydhof Hansen, Stefan Kowalewski, Kim G. Larsen and Mads Chr. Olesen
Automatic Derivation of Abstract Semantics From Instruction Set Descriptions
Dominique Gückel and Stefan Kowalewski
11:15 - 11:30 Coffee Break
11:30 - 12:30 Invited Talk
Making Sense of Relaxed-Memory Concurrency
Peter Sewell (University of Cambridge)
12:30 - 14:00 Lunch
14:00 - 15:00 Session II
Structuring Interactive Correctness Proofs by Formalizing Coding Idioms
Holger Gast
Verification of Dependable Software using Spark and Isabelle
Stefan Berghofer
15:00 - 15:30 Coffee Break
15:30 - 16:30 Invited Talk
VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java
Bart Jacobs (Katholieke Universiteit Leuven)
16:30 - 16:45 Coffee Break
16:45 - 17:45 Session III
Verification of Safety-Critical Systems: A Case Study Report on Using Modern Model Checking Tools
Antti Jääskeläinen, Mika Katara, Shmuel Katz and Heikki Virtanen
A Tool for the Certification of Sequential Function Charts based System Specifications
Jan Olaf Blech
20:00 Workshop Dinner (restaurant In geuren en kleuren)
Sponsored by:
NICTA
Supported by:
FBK RWTH-AACHEN Technische Universitat Dresden RWTH-AACHEN
Published by:
[to be announced]
Valid XHTML 1.0 Transitional Valid CSS! [Valid RSS]
Inspired by the FMICS 2010 web pages by Marco Roveri