tr-announce April 2011

tr-announce@lists.rwth-aachen.de

1 Teilnehmer
2 Diskussionen

2011-03: A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems

von Carsten Fuhs

The following technical report is available from http://aib.informatik.rwth-aachen.de: A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems Lars Noschinski, Fabian Emmes, Jürgen Giesl AIB 2011-03 We present a modular framework to analyze the innermost runtime complexity of term rewrite systems automatically. Our method is based on the dependency pair framework for termination analysis. In contrast to previous work, we developed a direct adaptation of successful termination techniques from the dependency pair framework in order to use them for complexity analysis. By extensive experimental results, we demonstrate the power of our method compared to existing techniques.

12 Jahre, 12 Monate

2011-02: Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting

von Carsten Fuhs

The following technical report is available from http://aib.informatik.rwth-aachen.de: Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting Marc Brockschmidt, Carsten Otto, Jürgen Giesl AIB 2011-02 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.

13 Jahre

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

tr-announce April 2011