License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2011.155
URN: urn:nbn:de:0030-drops-31146
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2011/3114/
Go to the corresponding LIPIcs Volume Portal

Brockschmidt, Marc ; Otto, Carsten ; Giesl, Jürgen

Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting

pdf-format:
7.pdf (0.7 MB)

Abstract

In earlier work we presented an approach to prove termination of
non-recursive Java Bytecode (JBC) programs automatically. Here,
JBC programs are first transformed to finite termination graphs
which represent all possible runs of the program.
Afterwards, the termination graphs are translated to term
rewrite systems (TRSs) such that termination of the resulting TRSs
implies termination of the original JBC programs. So in this way,
existing techniques and tools from term rewriting can be used to
prove termination of JBC automatically. In this paper, we improve
this approach substantially in two ways:

(1) We extend it in order to also analyze recursive JBC programs.
To this end, one has to represent call stacks of arbitrary
size.

(2) To handle JBC programs with several methods, we modularize our
approach in order to re-use termination graphs and TRSs for the
separate methods and to prove termination of the resulting TRS
in a modular way.

We implemented our approach in the tool AProVE. Our experiments show
that the new contributions increase the power of termination analysis
for JBC significantly.

BibTeX - Entry

@InProceedings{brockschmidt_et_al:LIPIcs:2011:3114,
  author =	{Marc Brockschmidt and Carsten Otto and J{\"u}rgen Giesl},
  title =	{{Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{155--170},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9 },
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Manfred Schmidt-Schau{\ss}},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3114},
  URN =		{urn:nbn:de:0030-drops-31146},
  doi =		{10.4230/LIPIcs.RTA.2011.155},
  annote =	{Keywords: termination, Java Bytecode, term rewriting, recursion}
}

Keywords: termination, Java Bytecode, term rewriting, recursion
Collection: 22nd International Conference on Rewriting Techniques and Applications (RTA'11)
Issue Date: 2011
Date of publication: 26.04.2011

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI