| Registration 8:30 - 9:00 |
Registration Registration
|
| Session 1 9:00 - 10:30 |
Welcome and Keynote Speech (chair: Jens
Knoop) Welcome and Opening
Jens Knoop Invited Keynote Speech: What Level of
Mathematical Reasoning can Computer Science Demand of a Software
Implementer
Hans Langmaack (Christian-Albrechts-Universität Kiel, Germany) (Chair: Jens Knoop) |
| Coffee |
|
| Session 2 11:00 - 12:20 |
(Chair: Markus Müller-Olm) Optimizing Code Generation from SSA Form: A
Comparison Between Two Formal Correctness Proofs in Isabelle/HOL
Jan Olaf Blech, Sabine Glesner, Johannes Leitner, Steffen Mülling (Universität Karlsruhe, Germany) Machine-Checkable Correctness Proofs for
Intra-procedural Dataflow Analyses
Alexandru Salcianu, Konstantine Arkoudas (MIT, USA) |
| Lunch |
|
| Session 3 14:00 - 15:20 |
(Chair: Sabine Glesner) Validating More Loop Optimizations
Ying Hu, Clark Barrett, Benjamin Goldberg (New York University, New York, USA), Amir Pnueli (Weizmann Institute, Israel) Automatically Inferring Sound Dataflow
Functions from Dataflow Fact Schemas
Erika Rice, Sorin Lerner, Craig Chambers (University of Washington, Seattle, USA) |
| Coffee |
|
| Session 4 16:00 - 18:00 |
(Chair: Wolf Zimmermann) Structural Encoding of Static Single
Assignment Form
Andreas Gal, Christian W. Probst, Michael Franz (University of California, Irvine, USA) Quantifying the Benefits of SSA-Based Mobile
Code
Wolfram Amme (Friedrich-Schiller-Universität Jena, Germany), Jeffery von Ronne, Michael Franz (University of California, Irvine, USA) 17:20-17:50 Panel: Verification of Optimizing
Compilers - Past and Future
Closing (Wolf Zimmermann)
|
| Evening 7.45pm for 8pm |
Dinner Dinner at Heights Rooftop Restaurant in the
Apex International Hotel, Grassmarket. Situated in one of Edinburgh's
oldest parts of town, the restaurant boasts a spectacular view of the
castle.
|