Title	Author(s)
Certifying Code Generation with Coq	Jan Olaf Blech (University of Kaiserslautern, Germany) and Benjamin Gregoire (INRIA Sophia-Antipoles, France)
Validation of Interprocedural Optimizations	Amir Pnueli and Anna Zaks (New York University, NY, USA)
Validating Correctness of Compiler Optimizer Execution Using Temporal Logic	Masataka Sassa and Soichiro Sahara (Tokyo Institute of Technology, Japan)
Proving Program Properties in Translation Validation	Andrei Voronkov (The University of Manchester, UK) and Iman Narasamdya (Verimag, Grenoble, France)
A Summary Function Model for the Validation of Interprocedural Analysis Results	Karsten Klohs (University of Paderborn, Germany)
A Formal Semantics of Intermediate Compiler Representations in Isabelle/HOL	Sabine Glesner and Andreas Humbert (Technical University of Berlin, Germany)