09:15-10:30

Objective Evidence of Software Quality: An Experience Report Kurt Wallnau (Carnegie Mellon University, Pittsburgh, PA, USA)

 
 

11:00-11:45

Validating Correctness of Compiler Optimizer Execution Using Temporal Logic Masataka Sassa and Soichiro Sahara (Tokyo Institute of Technology, Japan)

11:45-12:30

Proving Program Properties in Translation Validation Andrei Voronkov (The University of Manchester, UK) and Iman Narasamdya (Verimag, Grenoble, France)

 
 

14:30-15:15

Validation of Interprocedural Optimizations Amir Pnueli and Anna Zaks (New York University, NY, USA)

15:15-16:00

A Summary Function Model for the Validation of Interprocedural Analysis Results Karsten Klohs (University of Paderborn, Germany)

 
 

16:30-17:15

A Formal Semantics of Intermediate Compiler Representations in Isabelle/HOL Sabine Glesner and Andreas Humbert (Technical University of Berlin, Germany)

17:15-18:00

Certifying Code Generation with Coq Jan Olaf Blech (University of Kaiserslautern, Germany) and Benjamin Gregoire (INRIA Sophia-Antipoles, France)

 
 

18:00 - 18:20

Certifying Code Generation Runs with Coq: A Tool Description Jan Olaf Blech (University of Kaiserslautern, Germany) and Benjamin Gregoire (INRIA Sophia-Antipoles, France)