Publisher
Sponsor
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 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.
Program
| 09:15 | Welcome |
| 09:30 | Invited Speaker: Bart Jacobs (KU Leuven) VeriFast: A Powerful, Fast, Sound, Predictable Verifier for C and Java
VeriFast |
| 10:30 | coffee break |
| 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. |
| 12:30 | lunch |
| 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:00 | coffee break |
| 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.
|
Proceedings
The ETAPS proceedings are available. The ENTCS proceedings will be published soon.Important Dates
| December 25, 2010 | |
| December 25, 2010 | |
| January 21, 2011 | |
| February 8, 2011 |
Call For Papers
[.txt]Submission
Paper should be submitted through the easy chair page.Program Committee
- 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