Abstract
We introduce a technique to prove non-termination of term rewrite systems automatically. Our technique improves over previous approaches substantially, as it can also detect non-looping non-termination.
Supported by the DFG grant GI 274/5-3.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Brockschmidt, M., Ströder, T., Otto, C., Giesl, J.: Automated detection of non-termination and NullPointerExceptions for Java Bytecode. In: Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS. Springer, Heidelberg (to appear, 2012) Available from [1]
Geser, A., Zantema, H.: Non-looping string rewriting. Informatique Théorique et Applications 33(3), 279–302 (1999)
Geser, A., Hofbauer, D., Waldmann, J.: Termination proofs for string rewriting systems via inverse match-bounds. J. Automated Reasoning 34(4), 365–385 (2005)
Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and Disproving Termination of Higher-Order Functions. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 216–231. Springer, Heidelberg (2005)
Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006)
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. Journal of Automated Reasoning 37(3), 155–203 (2006)
Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. Information and Computation 199(1-2), 172–199 (2005)
Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean Termination Tool 2. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 295–304. Springer, Heidelberg (2009)
Oppelt, M.: Automatische Erkennung von Ableitungsmustern in nichtterminierenden Wortersetzungssystemen, Diploma Thesis, HTWK Leipzig, Germany (2008)
Payet, É.: Loop detection in term rewriting using the eliminating unfoldings. Theoretical Computer Science 403, 307–327 (2008)
Schernhammer, F., Gramlich, B.: VMTL–A Modular Termination Laboratory. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 285–294. Springer, Heidelberg (2009)
Waldmann, J.: Matchbox: A Tool for Match-Bounded String Rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 85–94. Springer, Heidelberg (2004)
Wang, Y., Sakai, M.: On non-looping term rewriting. In: WST 2006, pp. 17-21 (2006)
Zankl, H., Sternagel, C., Hofbauer, D., Middeldorp, A.: Finding and Certifying Loops. In: van Leeuwen, J., Muscholl, A., Peleg, D., Pokorný, J., Rumpe, B. (eds.) SOFSEM 2010. LNCS, vol. 5901, pp. 755–766. Springer, Heidelberg (2010)
Zantema, H.: Termination of string rewriting proved automatically. Journal of Automated Reasoning 34, 105–139 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Emmes, F., Enger, T., Giesl, J. (2012). Proving Non-looping Non-termination Automatically. In: Gramlich, B., Miller, D., Sattler, U. (eds) Automated Reasoning. IJCAR 2012. Lecture Notes in Computer Science(), vol 7364. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31365-3_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-31365-3_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31364-6
Online ISBN: 978-3-642-31365-3
eBook Packages: Computer ScienceComputer Science (R0)