{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T12:01:52Z","timestamp":1762862512284},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439974"},{"type":"electronic","value":"9783540456575"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45657-0_36","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T14:59:43Z","timestamp":1179586783000},"page":"442-454","source":"Crossref","is-referenced-by-count":65,"title":["Practical Methods for Proving Program Termination"],"prefix":"10.1007","author":[{"given":"Michael A.","family":"Col\u00f3n","sequence":"first","affiliation":[]},{"given":"Henny B.","family":"Sipma","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"36_CR1","doi-asserted-by":"crossref","unstructured":"Nikolaj S. Bj\u00f8rner, Anca Browne, Michael Col\u00f3n, Bernd Finkbeiner, Zohar Manna, Henny B. Sipma, and Tom\u00e1s E. Uribe. Verifying temporal properties of reactive systems: A STeP tutorial. Formal Methods in System Design, 16(3):227\u2013270, June 2000.","DOI":"10.1023\/A:1008700623084"},{"key":"36_CR2","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/S0167-6423(99)00008-8","volume":"35","author":"J. Brauburger","year":"1999","unstructured":"J. Brauburger and J. Giesl. Approximating the domains of functional and imperative programs. Science of Computer Programming, 35:113\u2013136, 1999.","journal-title":"Science of Computer Programming"},{"key":"36_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Proc. Second GI Conf. Autamata Theory and Formal Languages","author":"G. E. Collins","year":"1975","unstructured":"G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In H. Brakhage, editor, Proc. Second GI Conf. Autamata Theory and Formal Languages, volume 33 of Lecture Notes in Computer Science, pages134\u2013183, 1975."},{"key":"36_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45319-9_6","volume-title":"7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"M. Col\u00f3n","year":"2001","unstructured":"Michael Col\u00f3n and Henny Sipma. Synthesis of linear ranking functions. In Tiziana Margaria and Wang Yi, editors, 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2031 of LNCS, pages 67\u201381. Springer Verlag, April 2001."},{"key":"36_CR5","volume-title":"Introduction to Algorithms","author":"T. Cormen","year":"1990","unstructured":"T. Cormen, C. Leiserson, and R. Rivest. Introduction to Algorithms. McGraw-Hill, New York, 1990."},{"key":"36_CR6","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Rhadia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM Symp. Princ. of Prog. Lang., pages 238\u2013252. ACM Press, 1977.","DOI":"10.1145\/512950.512973"},{"key":"36_CR7","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Nicholas Halbwachs. Automatic discovery of linear restraints among the variables of a program. In 5th ACM Symp. Princ. of Prog. Lang., pages84\u201397, January 1978.","DOI":"10.1145\/512760.512770"},{"key":"36_CR8","unstructured":"Dennis Dams, Rob Gerth, and Orna Grumberg. A heuristic for the automatic generation of ranking functions. In Workshop on Advances in Verification (WAVe\u201900), pages 1\u20138, 2000."},{"key":"36_CR9","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3:69\u2013116, 1987.","journal-title":"Journal of Symbolic Computation"},{"key":"36_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/3-540-61576-8_77","volume-title":"Combinatorics and Computer Science","author":"K. Fukuda","year":"1996","unstructured":"K. Fukuda and A. Prodon. Double description method revisited. In Combinatorics and Computer Science, volume 1120 of Lecture Notes in Computer Science, pages91\u2013111. Springer-Verlag, 1996."},{"key":"36_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"426","DOI":"10.1007\/3-540-59200-8_77","volume-title":"Proc. 6th Intl. Conf. Rewriting Techniques and Applications","author":"J. Giesl","year":"1995","unstructured":"J. Giesl. Generating polynomial orderings for termination proofs. In J. Hsiang, editor, Proc. 6th Intl. Conf. Rewriting Techniques and Applications, volume 914 of Lecture Notes in Computer Science, pages 426\u2013431. Springer-Verlag, 1995."},{"key":"36_CR12","doi-asserted-by":"crossref","unstructured":"J. Giesl, C. Walther, and J. Brauburger. Termination analysis for functional programs. In W. Bibel and P. H. Schmitt, editors, Automated Deduction \u2014 A Basis for Applications, Volume III: Applications, chapter 6, pages 135\u2013164. Kluwer Academic, 1998.","DOI":"10.1007\/978-94-017-0437-3_6"},{"key":"36_CR13","unstructured":"Zohar Manna. Mathematical Theory of Computation. McGraw-Hill, 1974."},{"key":"36_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995."},{"issue":"20","key":"36_CR15","first-page":"199","volume":"19","author":"S. D de","year":"1994","unstructured":"D. de Schreye and S. Decorte. Termination of logic programs: The never ending story. Journal of Logic Programming, 19,20:199\u2013260, 1994.","journal-title":"Journal of Logic Programming"},{"key":"36_CR16","unstructured":"Niklaus Wirth. Algorithms + Data Structures = Programs. Prentice-Hall, 1976."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45657-0_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T05:21:03Z","timestamp":1556428863000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45657-0_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439974","9783540456575"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-45657-0_36","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}