08:55-10:00

Practical Applications of Compiler Verification Techniques in Developing Production Optimizing Compilers Robert Charles Morgan (IBM, USA)

10:00-10:30

Functional Elimination of Phi-Instructions Lennart Beringer (LMU Munich, Germany)

 
 

11:00-11:30

Generating Invariants for Translation Validation Yi Fang (Microsoft, Redmond, USA) and Lenore D. Zuck (University of Illinois at Chicago, USA)

11:30-12:00

Optimisation Validation David Aspinall (Univ. of Edinburgh, UK), Lennart Beringer (LMU Munich, Germany), and Alberto Momigliano (University of Edinburgh, UK, and University of Milano, Italy)

12:00-12:30

Coinductive Verification of Program Optimizations using Similarity Relations Sabine Glesner, Johannes Leitner, and Jan Olaf Blech (Technical University of Berlin, Germany)

 
 

14:00-14:30

Structuring Optimizing Transformations and Proving Them Sound Aditya Kanade, Amitabha Sanyal, and Uday Khedker (IIT Bombay, India)

14:30-15:00

Data-Flow Analysis as a General Concept for the Transport of Verifiable Programs Wolfram Amme, Marc-Andre Müller, and Philipp Adler (University of Jena, Germany)

15:00-15:30

Using Verified Data-Flow Analysis-based Optimizations in Attribute Grammars Eric Van Wyk and Lijesh Krishnan (University of Minnesota, USA)

 
 

16:00-17:10

What Level of Mathematical Reasoning can Computer Science Demand of a Software Implementer Hans Langmaack (Christian-Albrechts-Universität Kiel, Germany)