Deciding innermost loops

René Thiemann*, Jürgen Giesl, Peter Schneider-Kamp

*Kontaktforfatter for dette arbejde

Publikation: Kapitel i bog/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

Abstrakt

We present the first method to disprove innermost termination of term rewrite systems automatically. To this end, we first develop a suitable notion of an innermost loop. Second, we show how to detect innermost loops: One can start with any technique amenable to find loops. Then our novel procedure can be applied to decide whether a given loop is an innermost loop. We implemented and successfully evaluated our method in the termination prover AProVE.

OriginalsprogEngelsk
TitelRewriting Techniques and Applications - 19th International Conference, RTA 2008, Proceedings
Antal sider15
Publikationsdato13. aug. 2008
Sider366-380
ISBN (Trykt)3540705880, 9783540705888
DOI
StatusUdgivet - 13. aug. 2008
Begivenhed19th International Conference on Rewriting Techniques and Applications, RTA 2008 - Hagenberg, Østrig
Varighed: 15. jul. 200817. jul. 2008

Konference

Konference19th International Conference on Rewriting Techniques and Applications, RTA 2008
LandØstrig
ByHagenberg
Periode15/07/200817/07/2008
NavnLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind5117 LNCS
ISSN0302-9743

Citationsformater