Program Bytecode 2007
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