tr-announce

Download

tr-announce@lists.rwth-aachen.de

April 2012

1 participants
2 discussions

2012-06: Automated Termination Proofs for Java Programs with Cyclic Data
by Thomas Ströder 19 Apr '12

19 Apr '12

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.

1 0

2012-05: Automated Complexity Analysis for Prolog by Term Rewriting
by Thomas Ströder 04 Apr '12

04 Apr '12

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.

1 0