From: Marieke H. <m.h...@ut...> - 2012-02-23 12:36:52
|
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 http://wwwhome.ewi.utwente.nl/~marieke/Bytecode2012/ NOTE: DEADLINE FOR NORMAL REGISTRATION ETAPS IS CLOSING ON FEB 26, 2012 Program ======= 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. Organiser ========= Marieke Huisman, University of Twente, Netherlands. All questions about the workshop can be addressed to her via mail: M.H...@ut.... 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 |