Bytecode, such as produced by e.g. Java and .NET compilers, has become a topic of interest, both for industry and academia. The industrial interest mainly stems from the fact that bytecode is typically used in critical environments, such as the Internet and smart cards. Moreover, an important characteristic for bytecode is that it is device-independent and allows dynamic loading of classes. For researchers that wish to apply formal methods to bytecode, this dynamic nature of bytecode provides an extra challenge. In addition, also the unstructuredness of the code and the pervasive presence of the stack provide extra challenges for the analysis of bytecode.

This workshop will focus on the latest developments in the semantics,verification, analysis and transformation of bytecode. Both new theoretical results and tool demonstrations are welcome.