Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Brockschmidt, Marc; Otto, Carsten; Giesl, Jürgen http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-31146
URL:

; ;

Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting

pdf-format:


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 =		{http://dx.doi.org/10.4230/LIPIcs.RTA.2011.155},
  annote =	{Keywords: termination, Java Bytecode, term rewriting, recursion}
}

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


DROPS-Home | Fulltext Search | Imprint Published by LZI