July 15, Wednesday
12:00 – 14:00
Automated Termination Analysis for Java Bytecode
Graduate seminar
Lecturer : Carsten Otto
Affiliation : RWTH, Germany
Location : 201/37
Host : Graduate Seminar
We present an automated approach to prove termination of Java Bytecode programs
by automatically transforming them to term rewrite systems (TRSs). In this way,
the numerous techniques and tools developed for TRS termination can also be
used for imperative object-oriented programming languages that can be compiled
into Java Bytecode. Compared to direct termination analysis of imperative
programs, rewrite techniques have the advantage that they are very powerful for
algorithms on user-defined data structures, since they can automatically
generate suitable well-founded orders comparing arbitrary forms of terms.
Moreover, by using term rewriting with built-in integers, rewrite techniques
are also powerful for algorithms on pre-defined data structures like integers..