cl-banner

Deciding Innermost Loops

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

Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008), Lecture Notes in Computer Science 5117, pp. 366 – 380, 2008.

Abstract

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.

 

  PDF |    doi:10.1007/978-3-540-70590-1_25  |  © Springer

BibTeX 

@inproceedings{RTJGPS-RTA08,
author = "Ren{\'e} Thiemann and J{\"u}rgen Giesl and Peter Schneider-Kamp",
title = "Deciding Innermost Loops",
booktitle = "Proceedings of the 19th International Conference on Rewriting
Techniques and Applications",
series = "Lecture Notes in Computer Science",
volume = 5117,
publisher = "Springer-Verlag",
year = 2008,
pages = "366--380"
}
Nach oben scrollen