Programme of COCV at ETAPS 2006

(Fifth Workshop on Compiler Optimization Meets Compiler Verification)

Sunday, April 2

08:40 - 10:30 SESSION 1 (COCV, Sunday, April 2, room: EI 5)

Opening
Wolf Zimmermann (Univ. of Halle, D)
Invited Keynote Speech
Practical Applications of Compiler Verification Techniques in Developing Production Optimizing Compilers
Robert Charles Morgan (IBM, USA)
Presentation (chair: Wolf Zimmermann)
Functional Elmination of Phi-Instructions
Lennart Beringer (LMU Munich, D)

10:30 - 11:00 Coffee

11:00 - 12:30 SESSION 2 (COCV, Sunday, April 2, room: EI 5)

Presentations (chair: George C. Necula)
Generating Invariants for Translation Validation
Yi Fang (Microsoft, Redmond, US) and Lenore D. Zuck (Univ. of Illinois at Chicago, USA)
Optimisation Validation
David Aspinall (Univ. of Edinburgh, UK), Lennart Beringer (LMU Munich, D), and Alberto Momigliano (Univ. of Edinburgh, UK, and Univ. of Milano, I)
Coinductive Verification of Program Optimizations using Similarity Relations
Sabine Glesner, Johannes Leitner, and Jan Olaf Blech (Technical Univ. of Berlin, D)

12:30 - 14:00 Lunch

14:00 - 15:30 SESSION 3 (COCV, Sunday, April 2, room: EI 5)

Presentations (chair: Markus Müller-Olm)
Structuring Optimizing Transformations and Proving them Sound
Aditya Kanade, Amitabha Sanyal, and Uday Khedker (IIT Bombay, IND)
Data-Flow Analysis as a General Concept for the Transport of Verifiable Programs
Wolfram Amme, Marc-Andre Müller, Philipp Adler (Univ. of Jena, D)
Using Verified Data-Flow Analysis-based Optimizations in Attribute Grammars
Eric Van Wyk, Lijesh Krishnan (Univ. of Minnesota, USA)

15:30 - 16:00 Coffee

16:00 - 17:30 SESSION 4 (COCV, Sunday, April 2, room: EI 5)

Invited Keynote Speech (chair: Jens Knoop)
What Level of Mathematical Reasoning can Computer Science Demand of a Software Implementer?
Hans Langmaack (Christian-Albrechts-Univ. Kiel, D)
Closing
Jens Knoop (Vienna Univ. of Technology, A)

Further ETAPS 2006 Programme Information:

ETAPS 2006 | Top | HTML 4.01 | Last Update: 2006-03-23