Title	Author(s)
Structuring Optimizing Transformations and Proving them Sound	Aditya Kanade, Amitabha Sanyal, and Uday Khedker (IIT Bombay, India)
Using Verified Data-Flow Analysis-based Optimizations in Attribute Grammars	Eric Van Wyk and Lijesh Krishnan (University of Minnesota, USA)
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)
Generating Invariants for Translation Validation	Yi Fang (Microsoft, Redmond, USA) and Lenore D. Zuck (University of Illinois at Chicago, USA)
Optimisation Validation	David Aspinall (University 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)
Functional Elimination of Phi-Instructions	Lennart Beringer (LMU Munich, Germany)