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 devices (smart-cards, phones, etc.) applications, 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. 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 will focus on theoretical and practical aspects of semantics, verification, analysis, certification and transformation of bytecode.
|09:30||Invited Speaker: Bart Jacobs (KU Leuven)
VeriFast: A Powerful, Fast, Sound, Predictable Verifier for C and Java
|11:00||Aibek Sarimbekov, Philippe Moret, Walter Binder, Andreas Sewe, and Mira Mezini
Complete and Platform-independent Calling Context Profiling for the Java Virtual Machine
Calling context profiling collects statistics separately for each calling context. Complete calling context profiles that faithfully represent overall program execution are important for a sound analysis of program behavior, which in turn is important for program understanding, reverse engineering, and workload characterization. Many existing calling context profilers for Java rely on sampling or on incomplete instrumentation techniques, yielding incomplete profiles; others rely on Java Virtual Machine (JVM) modifications or work only with one specific JVM, thus compromising portability. In this paper we present a new calling context profiler for Java that reconciles completeness of the collected profiles and full compatibility with any standard JVM. In order to reduce measurement perturbation, our profiler collects platform-independent dynamic metrics, e.g., the number of method invocations and the number of executed bytecodes. In contrast to prevailing calling context profilers, our tool is able to distinguish between call sites and supports selective profiling of (the dynamic extent of) certain methods. We evaluate the overhead introduced by our profiler with standard Java and Scala benchmarks on a range of different JVMs.
|11:30||David Pearce and James Noble
Implementing Whiley on the JVM
Dynamically typed languages are flexible and impose few burdens on the programmer. In contrast, static typing leads to software that is more efficient and has fewer errors. However, static type systems traditionally require every variable to have one type, and that relationships between types (e.g. subclassing) be declared explicitly. The Whiley language aims to hit a sweet spot between dynamic and static typing. This is achieved through structural subtyping and by typing variables in a flow-sensitive fashion. Whiley compiles to the JVM, and this presents a number of challenges. In this paper, we discuss the implementation of Whiley's type system on the JVM.
|12:00||Jiin Park, Jinhyung Park, Wonjoon Song, Sungwook Yoon, Bernd Burgstaller, and Bernhard Scholz
Treegraph-based instruction scheduling for stack-based virtual machines
Given the growing interest in the JVM and Microsoft's CLI as programming language implementation targets, code generation techniques for efficient stack-code are required. Compiler infrastructures such as LLVM are attractive for their highly optimizing middleend. However, LLVM's intermediate representation is register-based, and an LLVM code generator for a stack-based virtual machine needs to bridge the fundamental differences of the register and stack-based computation models. In this paper we investigate how the semantics of a register-based IR can be mapped to stack-code. We introduce a novel program representation called treegraphs. Treegraph nodes encapsulate computations that can be represented by DFS trees. Treegraph edges manifest computations with multiple uses, which is inherently incompatible with the consuming semantics of stack-based operators. Instead of saving a multiply-used value in a temporary, our method keeps all values on the stack, which avoids costly store and load instructions. Code-generation then reduces to scheduling of treegraph nodes in the most cost-effective way.
|14:30||Diego Esteban Alonso Blas, Puri Arenas, and Samir Genaim
Handling non-linear operations in the value analysis of COSTA
Inferring precise relations between (the values of) program variables at different program points is essential for termination and resource usage analysis. In both cases, this information is used to synthesize ranking functions that imply the programs termination and bound the number of iterations of its loops. For efficiency, it is common to base value analysis on non-disjunctive abstract domains such as polyhedra, octagon, etc. While these domains are efficient and able to infer complex relations, they are often not sufficient for modeling the effect of non-linear (arithmetic) operations. Modeling such operations precisely normally requires the use of disjunctive abstract domains, at the price of performance overhead. In this paper we report on an implementation, in the context of COSTA (a COSt and Termination Analyser for Java bytecode), of a value analysis that is based on the idea of encoding the disjunctive nature of non-linear operations into the (abstract) program itself, instead of using disjunctive abstract domains. Our experiments demonstrates that COSTA is now able prove termination and infer upper-bounds for programs that could not handle before.
|15:00||Kenneth MacKenzie and Damon Fenacci
Static Resource Analysis for Java Bytecode Using Amortisation and Separation Logic
In this paper we describe a static analyser for Java bytecode which uses a combination of amortised analysis and Separation Logic due to Robert Atkey. With the help of Java annotations we are able to give precise resource utilisation constraints for Java methods which manipulate various heap-based data structures.
|15:30||Kari Kähkönen, Tuomas Launiainen, Olli Saarikivi, Janne Kauttio, Keijo Heljanko, and Ilkka Niemelä
LCT: An Open Source Concolic Testing Tool for Java Programs (Tool Paper)
LCT (LIME Concolic Tester) is an open source concolic testing tool for sequential Java programs. In concolic testing test cases are generated for a given program by executing it both concretely and symbolically at the same time. LCT instruments the bytecode of the program under test to enable symbolic execution and collects constraints on input values that can be used to guide the testing to previously unexplored execution paths. The tool also supports distributing the test generation and execution to multiple processes that can be run on a single machine or even on a network of computers. This paper describes the architecture behind LCT and demonstrates through benchmarks how the distributed nature of the tool makes test generation more scalable.
|16:30||Invited Speaker: Todd Mytkowicz (Microsoft Research)
Bytecode at Microsoft Research
Bytecode plays an important role in many of the projects in the RiSE group at Microsoft Research. This talk will explore some of the underlying (publicly available) infrastructure that has been produced to support the analysis, optimization, and instrumentation of .Net bytecode. The talk will also cover some of the tools that have been built on top of this infrastructure as part of various research projects by members of the RiSE group.
ProceedingsThe ETAPS proceedings are available. The ENTCS proceedings will be published soon.
|December 25, 2010|
|December 25, 2010|
|January 21, 2011|
|February 8, 2011|
Call For Papers[.txt]
SubmissionPaper should be submitted through the easy chair page.
- Pierre Ganty (co-chair), the IMDEA Software Institute, Spain
- Mark Marron (co-chair), the IMDEA Software Institute, Spain
- David Pichardie, INRIA Rennes, France
- Dejvuth Suwimonteerabuth, King Mongkut's University of Technology, Thailand
- Samir Genaim, Complutense University of Madrid, Spain
- Elvira Albert, Complutense University of Madrid, Spain
- Fausto Spoto, University of Verona, Italy
- Francesco Logozzo, Microsoft Research, USA
- Michael Emmi, LIAFA, France
- Darko Stefanovic, University of New Mexico, USA