| Session chair: Marieke Huisman | |
| 9:00 - 10:00 | Invited talk: Peter Müller (ETH Zurich) - Modular verification of object invariants in Spec# |
| 10:00 - 10:30 | Tarmo Uustalu and Ando Saabas (Tallinn University of Technology, Estonia) - Type Systems for optimising Stack-based Code |
| 10:30 - 11:00 | coffee break |
| 11:00 - 11:30 | Jaroslav Sevcik (University of Edinburgh, UK) - Proving Resource Consumption of Low-level and Programs using Automated Theorem Provers |
| 11:30 - 12:00 | Hermann Lehner and Peter Müller (ETH, Zurich, Switzerland) - Formal Translation of Bytecode into BoogiePL |
| 12:00 - 12:30 | Emilie Balland, Pierre-Etienne Moreau and Antoine Reilles (Loria, France) - Bytecode Rewriting in Tom |
| 12:30 - 14:00 | lunch |
| Session chair: Peter Müller | |
| 14:00 - 14:30 | Jesse McGeachie and Juergen Dingel (Queen's University, Canada) - Translate One, Analyze Many: Leveraging the Microsoft Intermediate Language and Source Code Transformation for Model Checking |
| 14:30 - 15:00 | Samir Genaim, Puri Arenas, Damiano Zanardini, German Puebla and Elvira Albert (Universidad Politécnica de Madrid, Universidad Complutense de Madrid, Spain) - Practical Assessment of Cost Analysis for Java Bytecode |
| 15:00 - 15:30 | Theo Ruys and Niels H.M. Aan de Brugh (University of Twente, The Netherlands) - MMC: the Mono Model Checker |
| 15:30 - 16:00 | Miguel Gomez-Zamalloa, Elvira Albert and German Puebla (Universidad Politécnica de Madrid, Universidad Complutense de Madrid, Spain) - Improving the Decompilation of Java Bytecode to Prolog by Partial Evaluation |
| 16:00 - 16:30 | coffee |
| Session chair: Fausto Spoto | |
| 16:30 - 17:00 | Quan Nguyen and Bernhard Scholz (University of New South Wales, University of Sydney, Australia) - Computing SSA Form with Matrices |
| 17:00 - 17:30 | Mario Méndez, Jorge Navas and Manuel Hermenegildo (University of New Mexico, USA) - An Efficient, Parametric Fixpoint Algorithm for Incremental Analysis of Java Bytecode |