MOVES Seminar 19 April 2010
Marc Brockschmidt
The Finite Interpretation Graph: A Versatile Source for Automated Termination Analysis of Java Bytecode
Abstract:
The halting problem, albeit known to be undecidable, has been studied extensively in the past years. Most approaches for termination analysis are restricted to logic programming languages and term rewriting, which are due to their clear, simple and (mostly) well-defined semantics a natural choice for analysis. However, most real-world programs are written using imperative languages, such as Java.
In this talk, I will present a symbolic evaluation framework for Java Bytecode, a low-level machine code-like variant of Java. The result of this symbolic evaluation is the finite interpretation graph, an over-approximation of all possible program runs starting in a given state.
The halting problem, albeit known to be undecidable, has been studied extensively in the past years. Most approaches for termination analysis are restricted to logic programming languages and term rewriting, which are due to their clear, simple and (mostly) well-defined semantics a natural choice for analysis. However, most real-world programs are written using imperative languages, such as Java.
In this talk, I will present a symbolic evaluation framework for Java Bytecode, a low-level machine code-like variant of Java. The result of this symbolic evaluation is the finite interpretation graph, an over-approximation of all possible program runs starting in a given state.
Christian von Essen
Automated Termination Analysis of Java Bytecode: From the Finite Interpretation Graph to Term Rewriting
Automated Termination Analysis of Java Bytecode: From the Finite Interpretation Graph to Term Rewriting
Abstract:
Term rewriting systems lend themselves very neatly to termination analysis, and there are some very powerful tools for this purpose. Hence it is natural to try to harvest the power of these utilities to analyze real-world programs written in imperative languages. To this end, it is necessary to transform programs into term rewriting systems.
In this talk, I will present how the finite interpretation graph can be used to achieve this goal for Java Bytecode. The main problem is the transformation of arbitrary data objects into terms.
Term rewriting systems lend themselves very neatly to termination analysis, and there are some very powerful tools for this purpose. Hence it is natural to try to harvest the power of these utilities to analyze real-world programs written in imperative languages. To this end, it is necessary to transform programs into term rewriting systems.
In this talk, I will present how the finite interpretation graph can be used to achieve this goal for Java Bytecode. The main problem is the transformation of arbitrary data objects into terms.
