| 1 | -- | 0 | Marieke Huisman, Fausto Spoto. Preface |
| 3 | -- | 18 | Jesse McGeachie, Jürgen Dingel. Translate One, Analyze Many: Leveraging the Microsoft Intermediate Language and Source Code Transformation for Model Checking |
| 19 | -- | 33 | Emilie Balland, Pierre-Etienne Moreau, Antoine Reilles. Bytecode Rewriting in Tom |
| 35 | -- | 50 | Hermann Lehner, Peter Müller. Formal Translation of Bytecode into BoogiePL |
| 51 | -- | 66 | Mario Méndez-Lojo, Jorge Navas, Manuel V. Hermenegildo. An Efficient, Parametric Fixpoint Algorithm for Analysis of Java Bytecode |
| 67 | -- | 83 | Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, Damiano Zanardini. Experiments in Cost Analysis of Java Bytecode |
| 85 | -- | 101 | Miguel Gómez-Zamalloa, Elvira Albert, Germán Puebla. Improving the Decompilation of Java Bytecode to Prolog by Partial Evaluation |
| 103 | -- | 119 | Ando Saabas, Tarmo Uustalu. Type Systems for Optimizing Stack-based Code |
| 121 | -- | 132 | Quan Hoang Nguyen, Bernhard Scholz. Computing SSA Form with Matrices |
| 133 | -- | 147 | Jaroslav Sevcík. Proving Resource Consumption of Low-level Programs Using Automated Theorem Provers |
| 149 | -- | 160 | Theo C. Ruys, Niels H. M. Aan de Brugh. MMC: the Mono Model Checker |