MOVES Seminar 24 Sep 2010, 9:30

Fabian Kürten

 

Automated Analysis of Side Effects in Java Bytecode  (Bachelor-Kolloquium)

 

Abstract:

 One current approach for proving termination of Java Bytecode programs
uses integer term rewrite systems.
In order to translate Java Bytecode programs the so-called termination
graph is used.
Unfortunately this approach is not well-suited for recursive programs.

In this talk we will present how we can detect the absence of
side-effects and the presence of referential transparency, and how we
can use this knowledge to represent recursive methods in the termination
graph.
We will then show how we can translate the new representation into an
ITRS.