tr-announce April 2012

tr-announce@lists.rwth-aachen.de

1 Teilnehmer
2 Diskussionen

2012-06: Automated Termination Proofs for Java Programs with Cyclic Data

von Thomas Ströder

The following technical report is available from http://aib.informatik.rwth-aachen.de: Automated Termination Proofs for Java Programs with Cyclic Data Marc Brockschmidt, Richard Musiol, Carsten Otto, and Jürgen Giesl AIB 2012-06 In earlier work, we developed a technique to prove termination of Java programs automatically: first, Java programs are automatically transformed to term rewrite systems (TRSs) and then, existing methods and tools are used to prove termination of the resulting TRSs. In this paper, we extend our technique in order to prove termination of algorithms on cyclic data such as cyclic lists or graphs automatically. We implemented our technique in the tool AProVE and performed extensive experiments to evaluate its practical applicability.

12 Jahre

2012-05: Automated Complexity Analysis for Prolog by Term Rewriting

von Thomas Ströder

The following technical report is available from http://aib.informatik.rwth-aachen.de: Automated Complexity Analysis for Prolog by Term Rewriting Thomas Ströder, Fabian Emmes, Jürgen Giesl, Peter Schneider-Kamp, and Carsten Fuhs AIB 2012-05 For term rewrite systems (TRSs), a huge number of automated termination analysis techniques have been developed during the last decades, and by automated transformations of Prolog programs to TRSs, these techniques can also be used to prove termination of Prolog programs. Very recently, techniques for automated termination analysis of TRSs have been adapted to prove asymptotic upper bounds for the runtime complexity of TRSs automatically. In this paper, we present an automated transformation from Prolog programs to TRSs such that the runtime of the resulting TRS is an asymptotic upper bound for the runtime of the original Prolog program (where the runtime of a Prolog program is measured by the number of unification attempts). Thus, techniques for complexity analysis of TRSs can now also be applied to prove upper complexity bounds for Prolog programs. Our experiments show that this transformational approach indeed yields more precise bounds than existing direct approaches for automated complexity analysis of Prolog. Moreover, it is also applicable to a larger class of Prolog programs such as non-well-moded programs or programs using built-in predicates like, e.g., cuts.

12 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 2012