@inproceedings{820cc6b71fc9444da6e0a3e6c17fea2a,
title = "Proving non-termination by finite automata",
abstract = "A new technique is presented to prove non-termination of term rewriting. The basic idea is to find a non-empty regular language of terms that is closed under rewriting and does not contain normal forms. It is automated by representing the language by a tree automaton with a fixed number of states, and expressing the mentioned requirements in a SAT formula. Satisfiability of this formula implies non-termination. Our approach succeeds for many examples where all earlier techniques fail, for instance for the S-rule from combinatory logic.",
author = "J. Endrullis and H. Zantema",
year = "2015",
doi = "10.4230/LIPIcs.RTA.2015.160",
language = "English",
isbn = "978-3-939897-85-9",
series = "LIPIcs: Leibniz International Proceedings in Informatics",
publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",
pages = "160--176",
editor = "M. Fern{\'a}ndez",
booktitle = "Rewriting Techniques and Applications (26th International Conference, RTA'15, Warsaw, Poland, June 29-July 3, 2015)",
note = "26th International Conference on Rewriting Techniques and Application (RTA 2015), RTA 2015 ; Conference date: 02-06-2015 Through 01-07-2015",
}