{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,16]],"date-time":"2026-05-16T05:50:54Z","timestamp":1778910654597,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642112652","type":"print"},{"value":"9783642112669","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11266-9_63","type":"book-chapter","created":{"date-parts":[[2009,12,7]],"date-time":"2009-12-07T09:04:58Z","timestamp":1260176698000},"page":"755-766","source":"Crossref","is-referenced-by-count":5,"title":["Finding and Certifying Loops"],"prefix":"10.1007","author":[{"given":"Harald","family":"Zankl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Sternagel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dieter","family":"Hofbauer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aart","family":"Middeldorp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1-2","key":"63_CR1","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T. Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of Term Rewriting Using Dependency Pairs. TCS\u00a0236(1-2), 133\u2013178 (2000)","journal-title":"TCS"},{"key":"63_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"63_CR3","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development; Coq\u2019Art: The Calculus of Inductive Constructions. In: Texts in Theoretical Computer Science. An EATCS Series (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"63_CR4","unstructured":"Blanqui, F., Delobel, W., Coupet-Grimal, S., Hinderer, S., Koprowski, A.: COLOR, a COQ Library on Rewriting and Termination. In: WST, pp. 69\u201373 (2006)"},{"issue":"1","key":"63_CR5","first-page":"7","volume":"19","author":"A. Clarke","year":"2001","unstructured":"Clarke, A., Biere, A., Raimi, R., Zhu, Y.: Bounded Model Checking Using Satisfiability Solving. FMSD\u00a019(1), 7\u201334 (2001)","journal-title":"FMSD"},{"key":"63_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-74621-8_10","volume-title":"Frontiers of Combining Systems","author":"E. Contejean","year":"2007","unstructured":"Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Certification of Automated Termination Proofs. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol.\u00a04720, pp. 148\u2013162. Springer, Heidelberg (2007)"},{"key":"63_CR7","doi-asserted-by":"crossref","unstructured":"Cook, S.: The Complexity of Theorem-Proving Procedures. In: STOC, pp. 151\u2013158 (1971)","DOI":"10.1145\/800157.805047"},{"key":"63_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"63_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"issue":"2-3","key":"63_CR10","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10817-007-9087-9","volume":"40","author":"J. Endrullis","year":"2008","unstructured":"Endrullis, J., Waldmann, J., Zantema, H.: Matrix Interpretations for Proving Termination of Term Rewriting. JAR\u00a040(2-3), 195\u2013220 (2008)","journal-title":"JAR"},{"issue":"4","key":"63_CR11","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/s10817-005-9024-8","volume":"34","author":"A. Geser","year":"2005","unstructured":"Geser, A., Hofbauer, D., Waldmann, J.: Termination Proofs for String Rewriting Systems via Inverse Match-Bounds. JAR\u00a034(4), 365\u2013385 (2005)","journal-title":"JAR"},{"issue":"3","key":"63_CR12","first-page":"279","volume":"33","author":"A. Geser","year":"1999","unstructured":"Geser, A., Zantema, H.: Non-Looping String Rewriting. TIA\u00a033(3), 279\u2013302 (1999)","journal-title":"TIA"},{"key":"63_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/978-3-540-32275-7_21","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Giesl","year":"2005","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 301\u2013331. Springer, Heidelberg (2005)"},{"key":"63_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/11559306_12","volume-title":"Frontiers of Combining Systems","author":"J. Giesl","year":"2005","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and Disproving Termination of Higher-Order Functions. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol.\u00a03717, pp. 216\u2013231. Springer, Heidelberg (2005)"},{"issue":"3","key":"63_CR15","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/s10817-006-9057-7","volume":"37","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and Improving Dependency Pairs. JAR\u00a037(3), 155\u2013203 (2006)","journal-title":"JAR"},{"key":"63_CR16","unstructured":"Haftmann, F.: Code Generation from Specifications in Higher Order Logic. PhD Thesis, Technische Universit\u00e4t M\u00fcnchen (2009)"},{"issue":"1-2","key":"63_CR17","first-page":"172","volume":"199","author":"N. Hirokawa","year":"2005","unstructured":"Hirokawa, N., Middeldorp, A.: Automating the Dependency Pair Method. I&C\u00a0199(1-2), 172\u2013199 (2005)","journal-title":"I&C"},{"key":"63_CR18","doi-asserted-by":"crossref","unstructured":"Korp, M., Middeldorp, A.: Match-Bounds Revisited. I&C (2009), doi:10.1016\/j.ic.2009.02.010","DOI":"10.1016\/j.ic.2009.02.010"},{"key":"63_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/978-3-642-02348-4_21","volume-title":"RTA 2009","author":"M. Korp","year":"2009","unstructured":"Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean Termination Tool\u00a02. In: Treinen, R. (ed.) RTA 2009. LNCS, vol.\u00a05595, pp. 295\u2013304. Springer, Heidelberg (2009)"},{"key":"63_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"63_CR21","unstructured":"Oppelt, M.: Automatische Erkennung von Ableitungsmustern in nichtterminierenden Wortersetzungssystemen. Master\u2019s Thesis, HTWK Leipzig, FH (2008)"},{"issue":"2-3","key":"63_CR22","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/j.tcs.2008.05.013","volume":"403","author":"\u00c9. Payet","year":"2008","unstructured":"Payet, \u00c9.: Loop Detection in Term Rewriting Using the Eliminating Unfoldings. TCS\u00a0403(2-3), 307\u2013327 (2008)","journal-title":"TCS"},{"issue":"3","key":"63_CR23","first-page":"293","volume":"2","author":"D. Plaisted","year":"1986","unstructured":"Plaisted, D., Greenbaum, S.: A Structure-Preserving Clause Form Translation. JSC\u00a02(3), 293\u2013304 (1986)","journal-title":"JSC"},{"key":"63_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"452","DOI":"10.1007\/978-3-642-03359-9_31","volume-title":"TPHOLs 2009","author":"R. Thiemann","year":"2009","unstructured":"Thiemann, R., Sternagel, C.: Certification of Termination Proofs Using CeTA. In: Berghofer, S., et al. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 452\u2013468. Springer, Heidelberg (2009)"},{"key":"63_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-3-540-25979-4_6","volume-title":"Rewriting Techniques and Applications","author":"J. Waldmann","year":"2004","unstructured":"Waldmann, J.: Matchbox: A Tool for Match-Bounded String Rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 85\u201394. Springer, Heidelberg (2004)"},{"key":"63_CR26","unstructured":"Waldmann, J.: Compressed Loops, Draft (2007), http:\/\/dfa.imn.htwk-leipzig.de\/matchbox\/methods\/loop.pdf"},{"key":"63_CR27","unstructured":"Zankl, H.: Lazy Termination Analysis. PhD Thesis, University of Innsbruck (2009)"},{"key":"63_CR28","doi-asserted-by":"crossref","unstructured":"Zantema, H.: Termination of String Rewriting Proved Automatically. JAR 34(2), 105\u2013139 (2005)","DOI":"10.1007\/s10817-005-6545-0"},{"key":"63_CR29","series-title":"Cambridge Tracts in Theoretical Computer Science","first-page":"181","volume-title":"Term Rewriting Systems","author":"H. Zantema","year":"2003","unstructured":"Zantema, H.: Termination. In: TeReSe (ed.) Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol.\u00a055, pp. 181\u2013259. Cambridge University Press, Cambridge (2003)"}],"container-title":["Lecture Notes in Computer Science","SOFSEM 2010: Theory and Practice of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11266-9_63","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,24]],"date-time":"2019-05-24T04:45:00Z","timestamp":1558673100000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11266-9_63"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642112652","9783642112669"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11266-9_63","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}