[isabelle] Bytecode'07: call for participation



==============================================================================

                           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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.