{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:50:17Z","timestamp":1775868617623,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540208037","type":"print"},{"value":"9783540246220","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24622-0_20","type":"book-chapter","created":{"date-parts":[[2010,9,5]],"date-time":"2010-09-05T11:33:53Z","timestamp":1283686433000},"page":"239-251","source":"Crossref","is-referenced-by-count":251,"title":["A Complete Method for the Synthesis of Linear Ranking Functions"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Podelski","sequence":"first","affiliation":[]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"20_CR1","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0304-3975(96)00191-0","volume":"173","author":"N. Bj\u00f8rner","year":"1997","unstructured":"Bj\u00f8rner, N., Browne, A., Manna, Z.: Automatic generation of invariants and intermediate assertions. Theoretical Computer Science\u00a0173(1), 49\u201387 (1997)","journal-title":"Theoretical Computer Science"},{"key":"20_CR2","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/S0304-3975(99)00034-1","volume":"221","author":"O. Burkart","year":"1999","unstructured":"Burkart, O., Steffen, B.: Model checking the full modal mucalculus for infinite sequential processes. Theoretical Computer Science\u00a0221, 251\u2013270 (1999)","journal-title":"Theoretical Computer Science"},{"key":"20_CR3","first-page":"84","volume-title":"Proc. of POPL 1978: Symp. on Principles of Programming Languages","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. of POPL 1978: Symp. on Principles of Programming Languages, pp. 84\u201397. ACM Press, New York (1978)"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45319-9_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Colon","year":"2001","unstructured":"Colon, M., Sipma, H.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 67\u201381. Springer, Heidelberg (2001)"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-45657-0_36","volume-title":"Computer Aided Verification","author":"M. Colon","year":"2002","unstructured":"Colon, M., Sipma, H.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 442\u2013454. Springer, Heidelberg (2002)"},{"key":"20_CR6","unstructured":"Dams, D., Gerth, R., Grumberg, O.: A heuristic for the automatic generation of ranking functions. In: Workshop on Advances in Verification (WAVe 2000), pp. 1\u20138 (2000)"},{"key":"20_CR7","series-title":"Prentice Hall Series in Automatic Computation","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall Series in Automatic Computation. Prentice Hall, Englewood Cliffs (1976)"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/3-540-47813-2_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Genaim","year":"2002","unstructured":"Genaim, S., Codish, M., Gallagher, J.P., Lagoon, V.: Combining norms to prove termination. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol.\u00a02294, pp. 126\u2013138. Springer, Heidelberg (2002)"},{"key":"20_CR9","volume-title":"Matrix Computations","author":"G.H. Golub","year":"1996","unstructured":"Golub, G.H., Van Loan, C.F.: Matrix Computations, 3rd edn. Johns Hopkins Univ. Press, Baltimore (1996)","edition":"3"},{"key":"20_CR10","unstructured":"Holzbaur, C.: OFAI clp(q,r) Manual, Edition 1.3.3. Austrian Research Institute for Artificial Intelligence, Vienna, TR-95-09 (1995)"},{"key":"20_CR11","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M. Karr","year":"1976","unstructured":"Karr, M.: Affine relationships among variables of a program. Acta Informatica\u00a06, 133\u2013151 (1976)","journal-title":"Acta Informatica"},{"key":"20_CR12","unstructured":"The Intelligent Systems Laboratory. SICStus Prolog User\u2019s Manual. Swedish Institute of Computer Science, PO Box 1263 SE-164 29 Kista, Sweden. Release 3.8.7 (October 2001)"},{"key":"20_CR13","first-page":"7","volume-title":"Proc. of JICSLP 1996: Joint Int. Conf. and Symp. on Logic Programming","author":"F. Mesnard","year":"1996","unstructured":"Mesnard, F.: Inferring left-terminating classes of queries for constraint logic programs. In: Maher, M.J. (ed.) Proc. of JICSLP 1996: Joint Int. Conf. and Symp. on Logic Programming, pp. 7\u201321. MIT Press, Cambridge (1996)"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/3-540-47764-0_6","volume-title":"Static Analysis","author":"F. Mesnard","year":"2001","unstructured":"Mesnard, F., Neumerkel, U.: Applying static analysis techniques for inferring termination conditions of logic programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol.\u00a02126, pp. 93\u2013110. Springer, Heidelberg (2001)"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Software model checking of liveness properties via transition invariants. Technical report, Max-Plank-Institut f\u00fcr Informatik (2003)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"20_CR16","volume-title":"Numerical Recipes in C: The Art of Scientific Computing","author":"W.H. Press","year":"1992","unstructured":"Press, W.H., Teukolsky, S.A., Vetterling, W.T., Flannery, B.P.: Numerical Recipes in C: The Art of Scientific Computing. Cambridge University Press, Cambridge (1992)"},{"key":"20_CR17","volume-title":"Theory of Linear and Integer Programming","author":"A. Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. John Wiley & Sons Ltd., Chichester (1986)"},{"key":"20_CR18","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1145\/113413.113433","volume-title":"Proc. of PODS 1991: Symp. on Principles of Database Systems","author":"K. Sohn","year":"1991","unstructured":"Sohn, K., Van Gelder, A.: Termination detection in logic programs using argument sizes. In: Proc. of PODS 1991: Symp. on Principles of Database Systems, pp. 216\u2013226. ACM Press, New York (1991)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24622-0_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,3]],"date-time":"2019-06-03T17:40:31Z","timestamp":1559583631000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24622-0_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208037","9783540246220"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24622-0_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}