{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T10:01:53Z","timestamp":1758708113399},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540252368"},{"type":"electronic","value":"9783540322757"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32275-7_22","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T21:14:41Z","timestamp":1292879681000},"page":"332-346","source":"Crossref","is-referenced-by-count":5,"title":["Automated Termination Analysis for Incompletely Defined Programs"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Walther","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephan","family":"Schweitzer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Acad. Press, NY (1979)"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/3-540-60360-3_38","volume-title":"Static Analysis","author":"J. Giesl","year":"1995","unstructured":"Giesl, J.: Termination Analysis for Functional Programs using Term Orderings. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol.\u00a0983, pp. 154\u2013171. Springer, Heidelberg (1995)"},{"key":"22_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1005797629953","volume":"19","author":"J. Giesl","year":"1997","unstructured":"Giesl, J.: Termination of Nested and Mutually Recursive Algorithms. Journal of Automated Reasoning\u00a019, 1\u201329 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"22_CR4","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-94-017-0437-3_6","volume-title":"Automated Deduction - A Basis for Applications","author":"J. Giesl","year":"1998","unstructured":"Giesl, J., Walther, C., Brauburger, J.: Termination Analysis for Functional Programs. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction - A Basis for Applications, vol.\u00a03, pp. 135\u2013164. Kluwer Acad. Publ., Dordrecht (1998)"},{"key":"22_CR5","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1142\/S0129054102001163","volume":"13","author":"F. Kamareddine","year":"2002","unstructured":"Kamareddine, F., Monin, F.: An extension of an automated termination method of recursive functions. Intern. J. of Found. of Comp. Sc.\u00a013, 361\u2013386 (2002)","journal-title":"Intern. J. of Found. of Comp. Sc."},{"key":"22_CR6","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/0304-3975(94)00021-2","volume":"135","author":"P. Manoury","year":"1994","unstructured":"Manoury, P., Simonot, M.: Automatizing Termination Proofs of Recursively Defined Functions. Theoretical Computer Science\u00a0135, 319\u2013343 (1994)","journal-title":"Theoretical Computer Science"},{"key":"22_CR7","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(99)00118-8","volume":"254","author":"F. Monin","year":"2001","unstructured":"Monin, F., Simonot, M.: An Ordinal Measure based Procedure for Termination of Functions. Theoretical Computer Science\u00a0254, 63\u201394 (2001)","journal-title":"Theoretical Computer Science"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Nielson, F., Nielson, H.R.: Termination Analysis based on Operational Semantics. Technical report, Aarhus University, Denmark (1995)","DOI":"10.7146\/dpb.v24i492.7020"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/3-540-61511-3_73","volume-title":"Automated Deduction - Cade-13","author":"C. Sengler","year":"1996","unstructured":"Sengler, C.: Termination of Algorithms over Non\u2212Freely Generated Data Types. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 121\u2013136. Springer, Heidelberg (1996)"},{"key":"22_CR10","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/0004-3702(94)90063-9","volume":"71","author":"C. Walther","year":"1994","unstructured":"Walther, C.: On Proving the Termination of Algorithms by Machine. Artificial Intelligence\u00a071, 101\u2013157 (1994)","journal-title":"Artificial Intelligence"},{"key":"22_CR11","unstructured":"http:\/\/www.verifun.de"},{"key":"22_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-540-45085-6_28","volume-title":"Automated Deduction \u2013 CADE-19","author":"C. Walther","year":"2003","unstructured":"Walther, C., Schweitzer, S.: About $\\surd$ eriFun. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 322\u2013327. Springer, Heidelberg (2003)"},{"key":"22_CR13","first-page":"35","volume":"32","author":"C. Walther","year":"2004","unstructured":"Walther, C., Schweitzer, S.: Verification in the Classroom. Journal of Automated Reasoning - Special Issue on Automated Reasoning and Theorem Proving in Education\u00a032, 35\u201373 (2004)","journal-title":"Journal of Automated Reasoning - Special Issue on Automated Reasoning and Theorem Proving in Education"},{"key":"22_CR14","unstructured":"Walther, C., Schweitzer, S.: Reasoning about Incompletely Defined Programs. Technical Report VFR 04\/02, Programmiermethodik, Technische Universit\u00e4t Darmstadt (2004)"},{"key":"22_CR15","doi-asserted-by":"crossref","first-page":"845","DOI":"10.1016\/B978-044450813-3\/50015-1","volume-title":"Handbook of Automated Reasoning","author":"A. Bundy","year":"2001","unstructured":"Bundy, A.: The Automation of Proof by Mathematical Induction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, pp. 845\u2013911. Elsevier, Amsterdam (2001)"},{"key":"22_CR16","doi-asserted-by":"crossref","first-page":"913","DOI":"10.1016\/B978-044450813-3\/50016-3","volume-title":"Handb. of Autom. Reasoning","author":"H. Comon","year":"2001","unstructured":"Comon, H.: Inductionless Induction. In: Robinson, A., Voronkov, A. (eds.) Handb. of Autom. Reasoning, vol.\u00a0I, pp. 913\u2013962. Elsevier, Amsterdam (2001)"},{"key":"22_CR17","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1093\/oso\/9780198537465.003.0003","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"C. Walther","year":"1994","unstructured":"Walther, C.: Mathematical Induction. In: Gabbay, D., Hogger, C., Robinson, J. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol.\u00a02, pp. 127\u2013228. Oxford University Press, Oxford (1994)"},{"key":"22_CR18","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/s100099900022","volume":"3","author":"S. Autexier","year":"2000","unstructured":"Autexier, S., Hutter, D., Langenstein, B., Mantel, H., Rock, G., Schairer, A., Stephan, W., Vogt, R., Wolpers, A.: VSE: Formal Methods Meet Industrial Needs. Intern. J. on Software Tools for Technology Transfer\u00a03, 66\u201377 (2000)","journal-title":"Intern. J. on Software Tools for Technology Transfer"},{"key":"22_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/3-540-48660-7_15","volume-title":"Automated Deduction - CADE-16","author":"S. Autexier","year":"1999","unstructured":"Autexier, S., Hutter, D., Mantel, H., Schairer, A.: inka 5.0 - A Logic Voyager. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 207\u2013211. Springer, Heidelberg (1999)"},{"key":"22_CR20","first-page":"523","volume":"1","author":"D. Hutter","year":"1996","unstructured":"Hutter, D., Langenstein, B., Sengler, C., Siekmann, J., Stephan, W., Wolpers, A.: Verification Support Environment (VSE). High Integrity Syst.\u00a01, 523\u2013530 (1996)","journal-title":"High Integrity Syst."},{"key":"22_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/3-540-61511-3_92","volume-title":"Automated Deduction - Cade-13","author":"D. Hutter","year":"1996","unstructured":"Hutter, D., Sengler, C.: INKA: The Next Generation. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 288\u2013292. Springer, Heidelberg (1996)"},{"key":"22_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/BFb0032751","volume-title":"Static Analysis","author":"J. Brauburger","year":"1997","unstructured":"Brauburger, J.: Automatic Termination Analysis for Partial Functions using Polynomial Orderings. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol.\u00a01302, pp. 330\u2013344. Springer, Heidelberg (1997)"},{"key":"22_CR23","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/S0167-6423(99)00008-8","volume":"35","author":"J. Brauburger","year":"1999","unstructured":"Brauburger, J., Giesl, J.: Approximating the Domains of Functional and Imperative Programs. Science of Computer Programming\u00a035, 113\u2013136 (1999)","journal-title":"Science of Computer Programming"},{"key":"22_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-60343-3_33","volume-title":"KI-95: Advances in Artificial Intelligence","author":"J. Giesl","year":"1995","unstructured":"Giesl, J.: Automated Termination Proofs with Measure Functions. In: Wachsmuth, I., Brauer, W., Rollinger, C.-R. (eds.) KI 1995. LNCS, vol.\u00a0981, pp. 149\u2013160. Springer, Heidelberg (1995)"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/3-540-48242-3_16","volume-title":"Logic Programming and Automated Reasoning","author":"J. Gow","year":"1999","unstructured":"Gow, J., Bundy, A., Green, I.: Extensions to the Estimation Calculus. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS, vol.\u00a01705, pp. 258\u2013272. Springer, Heidelberg (1999)"},{"key":"22_CR26","unstructured":"Hutter, D.: Using Rippling to Prove the Termination of Algorithms. Technical Report RR 97-03, DFKI, Saarbr\u00fccken (1997)"},{"key":"22_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1007\/3-540-61511-3_119","volume-title":"Automated Deduction - Cade-13","author":"D. McAllester","year":"1996","unstructured":"McAllester, D., Arkoudas, K.: Walther Recursion. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 643\u2013657. Springer, Heidelberg (1996)"},{"key":"22_CR28","unstructured":"Walther, C., Schweitzer, S.: Automated Termination Analysis for Incompletely Defined Programs. Technical Report VFR 04\/03, Programmiermethodik, Technische Universit\u00e4t Darmstadt (2004)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32275-7_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,2]],"date-time":"2024-04-02T05:20:43Z","timestamp":1712035243000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32275-7_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540252368","9783540322757"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32275-7_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}