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. © 2008 Springer-Verlag.
Cite
CITATION STYLE
Thiemann, R., Giesl, J., & Schneider-Kamp, P. (2008). Deciding innermost loops. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5117 LNCS, pp. 366–380). https://doi.org/10.1007/978-3-540-70590-1_25
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
