09:15-10:30

A Framework for Certified Compilation Xavier Rival (ENS Paris, France)

 
 

11:00-11:45

Completeness of Instruction Selector Specifications with Dynamic Checks Florian Brandner (Vienna University of Technology, Austria)

11:45-12:30

Timing Properties: Beyond Verifying Functional Program Properties Jens Knoop (Vienna University of Technology, Austria)

 
 

14:00-14:45

Verification of Compiler Optimization Using Temporal Logic by Checking Value Equality Difference Ling Fang and Masataka Sassa (Tokyo Institute of Technology, Japan)

14:45-15:30

Using Checker Predicates in Certifying Code Generation Jan Olaf Blech (University of Kaiserslautern, Germany) and Benjamin Gregoire (INRIA Sophia-Antipoles, France)

 
 

16:00-16:45

Verifying State Representation Changes: Correctness of Memory Mappings Wolf Zimmermann (Martin-Luther-University Halle-Wittenberg, Germany)

16:45-18:00

Static Benefits from Translation Validation Sorin Lerner (University of California at San Diego, CA, USA)