| 1 | -- | 2 | Jens Knoop, George C. Necula, Wolf Zimmermann. Preface |
| 3 | -- | 20 | Lennart Beringer. Functional Elimination of Phi-instructions |
| 21 | -- | 35 | Yi Fang, Lenore D. Zuck. Improved Invariant Generation for Tvoc |
| 37 | -- | 59 | David Aspinall, Lennart Beringer, Alberto Momigliano. Optimisation Validation |
| 61 | -- | 77 | Sabine Glesner, Johannes Leitner, Jan Olaf Blech. Coinductive Verification of Program Optimizations Using Similarity Relations |
| 79 | -- | 95 | Aditya Kanade, Amitabha Sanyal, Uday P. Khedker. Structuring Optimizing Transformations and Proving Them Sound |
| 97 | -- | 108 | Wolfram Amme, Marc-André Möller, Philipp Adler. Data Flow Analysis as a General Concept for the Transport of Verifiable Program Annotations |
| 109 | -- | 122 | Eric {Van Wyk}, Lijesh Krishnan. Using Verified Data-Flow Analysis-based Optimizations in Attribute Grammars |