| 1 | -- | 3 | Jens Knoop, George C. Necula, Wolf Zimmermann. Preface |
| 5 | -- | 17 | Sorin Lerner, Todd D. Millstein, Craig Chambers. Cobalt: A Language for Writing Provably-Sound Compiler Optimizations |
| 19 | -- | 35 | Sabine Glesner, Simone Forster, Matthias Jäger. A Program Result Checker for the Lexical Analysis of the GNU C Compiler |
| 37 | -- | 51 | Arnd Poetzsch-Heffter, Marek Gawkowski. Towards Proof Generating Compilers |
| 53 | -- | 71 | Benjamin Goldberg, Lenore D. Zuck, Clark W. Barrett. Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers |
| 73 | -- | 93 | Sabine Glesner. A Proof Calculus for Natural Semantics Based on Greatest Fixed Point Semantics |
| 95 | -- | 111 | Karsten Klohs, Uwe Kastens. Memory Requirements of Java Bytecode Verification on Limited Devices |
| 113 | -- | 129 | Elvira Albert, Germán Puebla, Manuel V. Hermenegildo. An Abstract Interpretation-based Approach to Mobile Code Safety |
| 131 | -- | 148 | Sid Ahmed Ali Touati. On the Optimality of Register Saturation |