Title	Author(s)
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)
Validating More Loop Optimizations	Ying Hu, Clark Barrett, Benjamin Goldberg (New York University, New York, USA), Amir Pnueli (Weizmann Institute, Israel)
Machine-Checkable Correctness Proofs for Intra-procedural Dataflow Analyses	Alexandru Salcianu, Konstantine Arkoudas (MIT, USA)
Automatically Inferring Sound Dataflow Functions from Dataflow Fact Schemas	Erika Rice, Sorin Lerner, Craig Chambers (University of Washington, Seattle, USA)
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)