[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] call for participation: Bytecode 2012 (an ETAPS 2012workshop), March 31, 2012 in Tallinn, Estonia

                    CALL FOR PARTICIPATION

                          Bytecode 2012
               Seventh Workshop on Bytecode Semantics,
               Verification, Analysis and Transformation

                  A Satellite workshop of ETAPS 2012
                           Tallinn, Estonia,
                            31 March 2012


9:00-10:00     Jeff Foster
                 Using bytecode transformation to retrofit fine-grained
                 security policies on unmodified Android
10:00-10:30     Olga Gadyatskaya, Eduardo Lostal and Fabio Massacci
                 Extended Abstract: Embeddable Security-by-Contract
                 Verifier for Java Card
10:30 - 11:00     Coffee Break
11:00 - 12:00     James Hunt
                 Bytecode and Safety-Critical Systems: Friend or Foe?
12:00 - 13:00     Henrik Soendberg Karlsen, Erik Ramsgaard Wognsen,
                 Mads Chr. Olesen and Rene Rydhof Hansen
                 Study, Formalisation, and Analysis of Dalvik Bytecode
12:30 - 14:00     Lunch Break
14:00 - 15:00     Diego Garbervetsky
                 Quantitative analysis of Java/.Net like programs to
                 understand heap memory requirements
15:00 - 15:30     Gabriele Costa, Giulio Caravagna, Giovanni Pardini and
                 Luca Wiegand
                 Log-based Lazy Monitoring of OSGi Bundles
15:30 - 16:00     Coffee Break
16:00 - 16:30     Elvira Albert, Samir Genaim and Guillermo RomĚn-D╠ez
                 Conditional Termination of Loops over Arrays
16:30 - 17:00     Michael Barnett and Shaz Qadeer
                 BCT: A translator from MSIL to Boogie

Description of the workshop
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 Internet and mobile device applications (smart
cards, 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 of formal
methods. Also the unstructuredness of the code and the pervasive
presence of the operand stack provide further challenges for the
analysis of bytecode. This workshop will focus on theoretical and
practical aspects of semantics, verification, analysis, certification
and transformation of bytecode.

Research on bytecode is an ideal test bench for the application of
formal methods to real languages. There is a major pressure in this
sense, because security is a hot topic for bytecode applications in
embedded devices. However, the scientific community on bytecode
semantics, verification, analysis, and transformation is currently
fragmented, and researchers often come from the two distinct worlds
of industry and academia. Therefore, the aim of our workshop is to let
researchers and practitioners from both the industrial and the
academic world present new or preliminary results and demonstrate new
software tools that are of interest for the community as a whole.

The workshop will be a mixture of extended abstracts, position papers,
and invited presentations. The goal is to make the workshop an active
discussion forum for all work related to bytecode.

Marieke Huisman, University of Twente, Netherlands.

All questions about the workshop can be addressed to her via mail:

Workshop Committee
Elvira Albert, Complutense University of Madrid, Spain
June Andronick, NICTA, Australia
Massimo Bartoletti, University of Cagliari, Italy
Lennart Beringer, Princeton University, USA
Marieke Huisman, University of Twente, Netherlands
Francesco Logozzo, Microsoft Research, USA
Peter Mueller, ETH Zuerich, Switzerland
Tamara Rezk, INRIA Sophia Antipolis-Mediterranee, France
Bernhard Scholz, University of Sydney, Australia
Fausto Spoto, University of Verona, Italy