DROPS

Document

DOI: 10.4230/LIPIcs.RTA.2011.155

Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting

Authors: Marc Brockschmidt, Carsten Otto, and Jürgen Giesl

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

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.

Cite as

Marc Brockschmidt, Carsten Otto, and Jürgen Giesl. Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 155-170, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{brockschmidt_et_al:LIPIcs.RTA.2011.155,
  author =	{Brockschmidt, Marc and Otto, Carsten and Giesl, J\"{u}rgen},
  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 =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.155},
  URN =		{urn:nbn:de:0030-drops-31146},
  doi =		{10.4230/LIPIcs.RTA.2011.155},
  annote =	{Keywords: termination, Java Bytecode, term rewriting, recursion}
}

Document

DOI: 10.4230/LIPIcs.RTA.2010.259

Automated Termination Analysis of Java Bytecode by Term Rewriting

Authors: Carsten Otto, Marc Brockschmidt, Christian von Essen, and Jürgen Giesl

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract

We present an automated approach to prove termination of Java Bytecode (JBC) programs by automatically transforming them to term rewrite systems (TRSs). In this way, the numerous techniques and tools developed for TRS termination can now be used for imperative object-oriented languages like Java, which can be compiled into JBC.

Cite as

Carsten Otto, Marc Brockschmidt, Christian von Essen, and Jürgen Giesl. Automated Termination Analysis of Java Bytecode by Term Rewriting. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 259-276, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{otto_et_al:LIPIcs.RTA.2010.259,
  author =	{Otto, Carsten and Brockschmidt, Marc and von Essen, Christian and Giesl, J\"{u}rgen},
  title =	{{Automated Termination Analysis of Java Bytecode by Term Rewriting}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{259--276},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.259},
  URN =		{urn:nbn:de:0030-drops-26570},
  doi =		{10.4230/LIPIcs.RTA.2010.259},
  annote =	{Keywords: Java Bytecode, termination, term rewriting}
}

Search Results

Documents authored by Otto, Carsten

Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting

Abstract

Cite as

Automated Termination Analysis of Java Bytecode by Term Rewriting

Abstract

Cite as

Thanks for your feedback!

Could not send message