09:10-10:30 Program Change

(Cancelled because of desease) What Level of Mathematical Reasoning can Computer Science Demand of a Software Implementer Hans Langmaack (Christian-Albrechts-Universität Kiel, Germany) NEW: Abstraction for Liveness or Never Take Completeness Theorems Too Seriously Amir Pnueli (The Weizmann Institute of Science, Rehovot, Israel)

 
 

11:00-11:40

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)

11:40-12:20

Machine-Checkable Correctness Proofs for Intra-procedural Dataflow Analyses Alexandru Salcianu, Konstantine Arkoudas (MIT, USA)

 
 

14:00-14:40

Validating More Loop Optimizations Ying Hu, Clark Barrett, Benjamin Goldberg (New York University, New York, USA), Amir Pnueli (Weizmann Institute, Israel)

14:40-15:20

Automatically Inferring Sound Dataflow Functions from Dataflow Fact Schemas Erika Rice, Sorin Lerner, Craig Chambers (University of Washington, Seattle, USA)

 
 

16:00-16:40

Structural Encoding of Static Single Assignment Form   Andreas Gal, Christian W. Probst, Michael Franz (University of California, Irvine, USA)

16:40-17:20

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