From: Fausto Spoto <fausto.spoto@univr.it>
==============================================================================
Call for Participation
Bytecode 2007
Second Workshop on Bytecode Semantics,
Verification, Analysis and Transformation
(European Joint Conferences on
Theory and Practice of Software)
March 31, 2007
Braga, Portugal
http://profs.sci.univr.it/~spoto/Bytecode07/
Registration:
http://www.di.uminho.pt/etaps07/
==============================================================================
Bytecode, such as produced by e.g. Java and .NET compilers, has become
an important topic of interest, both for industry and academia. The
industrial interest stems from the fact that bytecode is typically
used for the Internet and mobile devices (smartcards, phones, etc.),
where security is a major issue. Moreover, bytecode is
device-independent and allows dynamic loading of classes, which
provides an extra challenge for the application formal methods. In
addition,
the unstructuredness of the code and the pervasive presence of the
operand stack also provide extra challenges for the analysis of
bytecode.
This workshop focuses on the latest developments in the semantics,
verification, analysis, and transformation of bytecode. Both new
theoretical results and tool demonstrations are presented.
Workshop program:
Invited talk: Peter Mueller
(ETH Zurich)
Modular Verification of Object Invariants in Spec#
Tarmo Uustala and Ando Saabas
(Tallinn University of Technology, Estonia)
Type Systems for Optimising Stack-based Code
Jaroslav Sevcik
(University of Edinburgh, UK)
Proving Resource Consumption of Low-level and Programs
using Automated Theorem Provers
Hermann Lehner and Peter Mueller
(ETH, Zurich, Switzerland)
Formal Translation of Bytecode into BoogiePL
Emilie Balland, Pierre-Etienne Moreau and Antoine Reilles
(Loria, France)
Bytecode Rewriting in Tom
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
Samir Genaim, Puri Arenas, Damiano Zanardini, German Puebla and Elvira
Albert
(Universidad Politecnica de Madrid, Universidad Complutense de Madrid,
Spain)
Practical Assessment of Cost Analysis for Java Bytecode
Theo Ruys and Niels H.M. Aan de Brugh
(University of Twente, The Netherlands)
MMC: the Mono Model Checker
Miguel Gomez-Zamalloa, Elvira Albert and German Puebla
(Universidad Politecnica de Madrid, Universidad Complutense de Madrid,
Spain)
Improving the Decompilation of Java Bytecode to Prolog by Partial
Evaluation
Quan Nguyen and Bernhard Scholz
(University of New South Wales, University of Sydney, Australia)
Computing SSA Form with Matrices
Mario Mendez, Jorge Navas and Manuel Hermenegildo
(University of New Mexico, USA)
An Efficient, Parametric Fixpoint Algorithm for Incremental Analysis
of Java Bytecode
Program committee:
Frederic Besson, IRISA, France
Samir Genaim, Universidad Politecnica de Madrid, Spain
Marieke Huisman, INRIA Sophia Antipolis, France (co-chair)
Francesco Logozzo, Microsoft Research, USA
Peter Mueller, ETH Zurich, Switzerland
Erik Poll, Radboud University Nijmegen, The Netherlands
Fausto Spoto, Universita' di Verona, Italy (co-chair)
Jan Vitek, Purdue University, USA
Last updated: Nov 21 2024 at 12:39 UTC