Peter Mueller

ETH Zurich, Switzerland

Abstract:

The talk describes a methodology for specifying and verifying object-oriented programs, using object invariants to specify the consistency of data, using ownership to organize objects into dynamic contexts, and using visibility to verify programs that escape an ownership structure. The methodology is designed to allow modular reasoning, even in the presence of subclasses and callbacks.

Tarmo Uustalu and Ando Saabas

Tallinn University of Technology, Estonia

Abstract:

We give a uniform type-systematic account of a number of optimizations and the underlying analyses for a bytecode-like stack-based low-level language, including analysis algorithms and soundness proofs. Specifically, we treat dead store instructions, load-pop pairs, duplicating load instructions, store-load pairs. The load-pop pairs and store-load pairs elimination optimizations are built on top of bidirectional analyses, facilitating correct elimination of instruction pairs spanning across basic block boundaries. As a result, no assumptions are needed about input code (it need not be the compiled form of a high-level source program, the stack need not be empty at basic block boundaries and not even need it be checked for safety before the analysis). The strongest analysis algorithms and soundness proofs are simple and uniform.

Jaroslav Sevcik

The University of Edinburgh, UK

Abstract:

In this paper we use a program logic and automatic theorem provers to certify resource usage of low-level bytecode programs equipped with annotations describing resource consumption for methods. We have adapted an existing resource counting logic (Aspinall et al., 2004) to fit the first-order setting, implemented a verification condition generator, and tested our approach on non-trivial recursive programs. We have successfully applied our framework to programs that did not involve any updates to recursive data structures. But mutation is more tricky because of aliasing of heap. We discuss problems related to this and suggest techniques to solve them.

Hermann Lehner and Peter Muller

ETH, Zurich, Switzerland

Abstract:

Many modern program verifiers translate the program to be verified and its specification into a simple intermediate representation and then compute verification conditions on this representation. Using an intermediate language improves the interoperability of tools and facilitates the computation of small verification conditions. Even though the translation into an intermediate representation is critical for the soundness of a verifier, this step has not been formally verified. In this paper, we formalize the translation of a small subset of Java bytecode into an imperative intermediate language similar to the intermediate language BoogiePL. We prove soundness of the translation by showing that each bytecode methods whose BoogiePL translation can be verified, can also be verified in a logic that operates directly on bytecode.

Emilie Balland, Pierre-Etienne Moreau and Antoine Reilles

Loria, France

Abstract:

In this paper, we present a term rewriting based library for manipulating Java bytecode. We define a mapping from bytecode programs to algebraic terms, and we use Tom, an extension of Java that adds pattern-matching facilities, to describe transformations. An originality of Tom is to provide a powerful strategy language to express traversals over trees and to control how transformation rules are applied. To be even more expressive, we use CTL formulae as conditions and we show how their satisfiability can be ensured using the strategy formalism. Through small examples, we show how bytecode analysis and transformations can be defined in an elegant way. In particular, we outline the implementation of a ClassLoader parameterized by a security policy that restricts file access.

Jesse McGeachie and Juergen Dingel

Queen's University, Canada

Abstract:

In this paper we present a source transformation-based framework to support model checking of source code written with languages belonging to Microsoft's .NET platform. The framework includes a set of source transformation rules to guide the transformation, tools to support assertion checking, as well as a tool for the automation of deadlock detection. The framework results in both executable and formally verifiable artifacts. We provide details of the tools in the framework, and evaluate the framework on a few small case studies.

Samir Genaim, Puri Arenas, Damiano Zanardini, German Puebla and Elvira Albert

Universidad Politécnica de Madrid, Universidad Complutense de Madrid, Spain

Abstract:

Recently we have proposed a general framework for the cost analysis of Java bytecode. This analysis generates, at compile-time, cost relations which define the cost of programs as a function of their input data size. The aim of this paper is to assess the practicality of this approach by experimentally evaluating a prototype implementation of the analysis in Ciao. The benchmarks considered include several well-known algorithms which have been used to evaluate existing cost analyzers in other programming paradigms. We also consider other benchmarks which illustrate object-oriented features. First, we evaluate whether the automatically generated cost relations can be solved by using the Mathematica system. Our experiments show that in some cases the cost relations inferred can be automatically solved, whereas in other cases, some manipulation is required, but then again they are automatically solvable. Second, we have experimentally evaluated the running times of the different phases of the analysis process. We believe that our experiments show that the efficiency of our cost analysis is acceptable and that the cost relations obtained are useful in practice since, at least in our experiments, it is possible to obtain a closed form solution.

Theo Ruys and Niels H.M. Aan de Brugh

University of Twente, The Netherlands

Abstract:

The Mono Model Checker (MMC) is a software model checker for CIL bytecode programs. MMC has been developed on the Mono platform. MMC is able to detect deadlocks and assertion violations in CIL programs. The design of MMC is inspired by the Java PathFinder (JPF), a model checker for Java programs. The performance of MMC is comparable to JPF. This paper introduces MMC and presents its main architectural characteristics.

Miguel Gomez-Zamalloa, Elvira Albert and German Puebla

Universidad Politécnica de Madrid, Universidad Complutense de Madrid, Spain

Abstract:

The interpretative approach to compilation allows compiling programs by partially evaluating an interpreter w.r.t. a source program. This approach, though very attractive in principle, has not been widely applied in practice mainly because of the difficulty in finding a partial evaluation strategy which always obtain quality compiled programs. In spite of this, in recent work we have performed a proof of concept of that, at least for some examples, this approach can be applied to decompile Java bytecode into Prolog. This allows applying existing advanced tools for analysis of logic programs in order to verify Java bytecode. However, successful partial evaluation of an interpreter for (a realistic subset of) Java bytecode is a rather challenging problem. The aim of this work is to improve the performance of the decompilation process above in two respects. First, we would like to obtain quality decompiled programs, i.e., simple and small. We refer to this as the effectiveness of the decompilation. Second, we would like the decompilation process to be as efficient as possible, both in terms of time and memory usage, in order to scale up in practice. We refer to this as the efficiency of the decompilation. With this aim, we propose several techniques for improving the partial evaluation strategy. We argue that the experimental results we present show that our techniques greatly improve the efficiency and effectiveness of the decompilation process.

Quan Nguyen and Bernhard Scholz

The University of New South Wales and The University of Sydney, Australia

Abstract:

Static Single-Assignment (SSA) form is an efficient intermediate representation used in virtual machines and modern compilers. It provides data flow information that simplifies the implementation of standard program optimisations such as constant propagation, dead code elimination, etc. Constructing SSA form involves the computation of graph relations such as dominance, and non-iterated and iterated dominance frontier. Although there exist efficient graph algorithms for these relations, the algorithms are elaborate to implement. In this paper we introduce a new approach to compute the dominance relation, the dominance frontiers, and the iterated dominance frontiers based on Boolean matrix calculus. We implemented our approach in an optimising backend for the LCC bytecode and compared its performance with the state-of-the-art approaches. We use the Spec95 benchmark suite for our experimental evaluation.

Mario Méndez, Jorge Navas and Manuel Hermenegildo

University of New Mexico, USA

Abstract:

Abstract interpretation has been widely used for the analysis of object-oriented languages and, more precisely, Java source and bytecode. However, while most of the existing work deals with the problem of finding expressive abstract domains that track accurately the characteristics of a particular concrete property, the underlying fixpoint algorithms have received comparatively less attention. In fact, many existing (abstract interpretation based) fixpoint algorithms rely on relatively inefficient techniques to solve inter-procedural call graphs or are specific and tied to particular analyses. We argue that the design of an efficient fixpoint algorithm is pivotal to support the analysis of large programs. In this paper we introduce a novel algorithm for analysis of Java bytecode which includes a number of optimizations in order to reduce the number of iterations. Also, the algorithm is parametric in the sense that it is independent of the abstract domain used and it can be applied to different domains as plug-ins. It is also incremental in the sense that, if desired, analysis data can be saved so that only a reduced amount of reanalysis is needed after a small program change, which can be instrumental for large programs. The algorithm is also multivariant and flow-sensitive. Finally, another interesting characteristic of the algorithm is that it is based on a program transformation, prior to the analysis, that results in a highly uniform representation of all the features in the language and therefore simplifies analysis. Detailed descriptions of decompilation solutions are provided and discussed with an example.