Compiler Optimization Meets Compiler Verification COCV 2006  

Final Program
(talks scheduled for 25+5min.)
Sunday, April 2, 2006
Location: To be announced


Registration: 08:00 - 08:45

Welcome and Opening: 08:40 - 08:50 (Wolf Zimmermann)


Session 1a: 08:50 - 10:00 Invited Keynote Speech (Chair: Wolf Zimmermann)


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

Session 1b: 10:00 - 10:30 (Chair: Wolf Zimmermann)


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


Coffee Break: 10:30 - 11:00


Session 2: 11:00 - 12:30 (Chair: George Necula )


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


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)


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


Lunch: 12:30 - 14:00

Session 3: 14:00 - 15:30 (Chair: Markus Müller-Olm)


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


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)


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


Coffee Break: 15:30 - 16:00


Session 4: 16:00 - 17:10 Invited Keynote Speech (Chair: Jens Knoop)


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


Closing: 17:10-17:20 (Jens Knoop)


Workshop Dinner: ca. 19:00 - ...