Workshop Description

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, tablets, etc.), where security is a major issue. Moreover, bytecode is device independent and allows dynamic loading of classes, which introduces an extra challenge for the application of formal methods. Also, the unstructuredness of the code and the pervasive presence of the operand stack result in 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.

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. No formal proceedings of the workshop will be published, but selected papers will be invited for a special issue of Science of Computer Programming.

Important Dates

  • Abstract submission deadline:
  • December 9, 2012     December 23, 2012
  • Paper submission deadline:
  • December 16, 2012    December 28, 2012
  • Author notification:
  • January 21, 2013
  • Camera-ready paper versions due:
  • February 8, 2013

    Call For Papers



    We solicit extended abstracts and position papers of at most 8 pages, describing work related to semantics, verification, analysis and transformation. In particular, we explicitly welcome tool demonstrations. Submissions may overlap with submissions to other conferences or journals. There will be a light-weight reviewing process, where submissions will be judged on their interest to the workshop audience.

    There will not be any formal proceedings of the workshop. All accepted submissions will be distributed among the workshop participants. After the workshop, presenters of extended abstracts, position papers, tool demos and of invited presentations may be invited to contribute to a special issue of Science of Computer Programming. Invitations will be based on submissions and presentations.

    Papers can be submitted (as PDF) through the easy chair page.

    Program Committee

    Program Chairs

    Miguel Gomez-Zamalloa Complutense University of Madrid, Spain
    Germán Puebla Technical University of Madrid, Spain

    Program Committee

    Richard Bubel Technische Universität Darmstadt
    Andrew Craik Oracle Labs, Brisbane, Australia
    Jürgen Giesl RWTH Aachen
    Laurent Hubert Prove&Run
    Marieke Huisman University of Twente
    Francesco Logozzo Microsoft Research
    Mark Marron IMDEA Software Institute
    Corina Pasareanu CMU/NASA Ames Research Center
    Ricardo Peña Complutense University of Madrid
    David Pichardie INRIA Rennes - Bretagne Atlantique
    Fausto Spoto Dipartimento di Informatica, Verona

    Invited Talks

    Wolfgang Ahrendt Chalmers University of Technology
    Étienne Payet LIM-IREMIA, Université de la Réunion, France


    (including slides)

    09:15 Welcome
    09:30 Invited Speaker: Wolfgang Ahrendt
    Developments in Object-Oriented Source Code Verification - an Inspiration for Bytecode Verification?
    10:30 José Miguel Rojas and Corina Pasareanu
    Compositional Symbolic Execution through Program Specialization (slides)
    11:00 coffee break
    11:30 Aibek Sarimbekov, Yudi Zheng, Danilo Ansaloni, Lubomir Bulej, Lukas Marek, Walter Binder, Petr Tuma and Zhengwei Qi.
    Java Bytecode Instrumentation – Reconciling Developer Productivity (slides)
    12:00 Andrey Breslav, Evgeny Geraschenko, Svetlana Isakova and Alexey Sedunov
    KAnnotator: Inferring precise type information from Java byte codes (slides)
    12:30 lunch
    14:00 Invited Speaker: Etienne Payet
    Modeling the Android platform (slides)
    15:00 Marieke Huisman and Matej Mihelčić
    Specification and Verification of GPGPU programs using Permission-based Separation logic (slides)
    15:30 coffee break
    16:00 Enrico Scapin and Fausto Spoto
    Field-Sensitive Unreachability and Non-Cyclicity Analysis (slides)
    16:30 Michael Barnett, Mehdi Bouaziz, Manuel Fahndrich and Francesco Logozzo
    A Case for Static Analyzers in the Cloud (Position paper) (slides)
    17:00 Pavle Subotic, Andrew Edward Santosa and Bernhard Scholz
    Static Analysis by Elimination (slides)