{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:46:44Z","timestamp":1770284804511,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642182747","type":"print"},{"value":"9783642182754","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-18275-4_26","type":"book-chapter","created":{"date-parts":[[2011,1,17]],"date-time":"2011-01-17T05:06:38Z","timestamp":1295240798000},"page":"371-386","source":"Crossref","is-referenced-by-count":1,"title":["Decision Procedures for Automating Termination Proofs"],"prefix":"10.1007","author":[{"given":"Ruzica","family":"Piskac","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"publisher","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":"26_CR2","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning","author":"L. Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Handbook of Automated Reasoning, pp. 19\u201399. MIT Press, Cambridge (2001)"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/11817963_35","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2006","unstructured":"Berdine, J., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Automatic termination proofs for programs with shape-shifting heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 386\u2013400. Springer, Heidelberg (2006)"},{"key":"26_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.A. Col\u00f3n","year":"2001","unstructured":"Col\u00f3n, M.A., Sipma, H.B.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 67\u201381. Springer, Heidelberg (2001)"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/11547662_8","volume-title":"Static Analysis","author":"B. Cook","year":"2005","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 87\u2013101. Springer, Heidelberg (2005)"},{"key":"26_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/11817963_37","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: terminator: Beyond safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 415\u2013418. Springer, Heidelberg (2006)"},{"issue":"7","key":"26_CR7","doi-asserted-by":"publisher","first-page":"1045","DOI":"10.1016\/j.ic.2006.03.002","volume":"204","author":"Y. Deng","year":"2006","unstructured":"Deng, Y., Sangiorgi, D.: Ensuring termination by typability. Inf. Comput.\u00a0204(7), 1045\u20131082 (2006)","journal-title":"Inf. Comput."},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems. In: Symposium on Foundations of Computer Science (SFCS), pp. 123\u2013131 (1979)","DOI":"10.1109\/SFCS.1979.32"},{"issue":"8","key":"26_CR9","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Commun. ACM\u00a022(8), 465\u2013476 (1979)","journal-title":"Commun. ACM"},{"issue":"2","key":"26_CR10","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/BF01237233","volume":"28","author":"J. Dick","year":"1990","unstructured":"Dick, J., Kalmus, J., Martin, U.: Automating the Knuth Bendix Ordering. Acta Inf.\u00a028(2), 95\u2013119 (1990)","journal-title":"Acta Inf."},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proc. Amer. Math. Soc. Symposia in Applied Mathematics, vol.\u00a019, pp. 19\u201331 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-540-78800-3_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Ihlemann","year":"2008","unstructured":"Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 265\u2013281. Springer, Heidelberg (2008)"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-642-02658-4_29","volume-title":"Computer Aided Verification","author":"S. Jacobs","year":"2009","unstructured":"Jacobs, S.: Incremental instance generation in local reasoning. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 368\u2013382. Springer, Heidelberg (2009)"},{"key":"26_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-642-15205-4_5","volume-title":"Computer Science Logic","author":"V. Kuncak","year":"2010","unstructured":"Kuncak, V., Piskac, R., Suter, P.: Ordered sets in the calculus of data structures. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol.\u00a06247, pp. 34\u201348. Springer, Heidelberg (2010)"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL, pp. 81\u201392 (2001)","DOI":"10.1145\/360204.360210"},{"key":"26_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/11541868_23","volume-title":"Theorem Proving in Higher Order Logics","author":"F.-J. Mart\u00edn-Mateos","year":"2005","unstructured":"Mart\u00edn-Mateos, F.-J., Ruiz-Reina, J.-L., Alonso, J.-A., Hidalgo, M.J.: Proof pearl: A formal proof of higman\u2019s lemma in ACL2. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 358\u2013372. Springer, Heidelberg (2005)"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/10703163_26","volume-title":"Computer Science Logic","author":"P. Narendran","year":"1999","unstructured":"Narendran, P., Rusinowitch, M., Verma, R.M.: RPO Constraint Solving Is in NP. In: Gottlob, G., Grandjean, E., Seyr, K. (eds.) CSL 1998. LNCS, vol.\u00a01584, pp. 385\u2013398. Springer, Heidelberg (1999)"},{"issue":"2","key":"26_CR18","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM TOPLAS\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM TOPLAS"},{"issue":"2","key":"26_CR19","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/0020-0190(93)90226-Y","volume":"47","author":"R. Nieuwenhuis","year":"1993","unstructured":"Nieuwenhuis, R.: Simple LPO constraint solving methods. Inf. Process. Lett.\u00a047(2), 65\u201369 (1993)","journal-title":"Inf. Process. Lett."},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-540-78163-9_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Piskac","year":"2008","unstructured":"Piskac, R., Kuncak, V.: Decision procedures for multisets with cardinality constraints. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 218\u2013232. Springer, Heidelberg (2008)"},{"key":"26_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-70545-1_25","volume-title":"Computer Aided Verification","author":"R. Piskac","year":"2008","unstructured":"Piskac, R., Kuncak, V.: Linear arithmetic with stars. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 268\u2013280. Springer, Heidelberg (2008)"},{"key":"26_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"26_CR23","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS 2004 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"issue":"3","key":"26_CR24","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/1232420.1232422","volume":"29","author":"A. Podelski","year":"2007","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. ACM TOPLAS\u00a029(3), 15 (2007)","journal-title":"ACM TOPLAS"},{"key":"26_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/11532231_16","volume-title":"Automated Deduction \u2013 CADE-20","author":"V. Sofronie-Stokkermans","year":"2005","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 219\u2013234. Springer, Heidelberg (2005)"},{"key":"26_CR26","doi-asserted-by":"crossref","unstructured":"Sofronie-Stokkermans, V., Ihlemann, C.: Automated reasoning in some local extensions of ordered structures. In: ISMVL (2007)","DOI":"10.1109\/ISMVL.2007.10"},{"key":"26_CR27","doi-asserted-by":"crossref","unstructured":"Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL (2010)","DOI":"10.1145\/1706299.1706325"},{"issue":"2","key":"26_CR28","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1145\/23005.24037","volume":"34","author":"K.N. Venkataraman","year":"1987","unstructured":"Venkataraman, K.N.: Decidability of the purely existential fragment of the theory of term algebras. Journal of the ACM (JACM)\u00a034(2), 492\u2013510 (1987)","journal-title":"Journal of the ACM (JACM)"},{"key":"26_CR29","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-45620-1_30","volume-title":"Automated Deduction - CADE-18","author":"C.G. Zarba","year":"2002","unstructured":"Zarba, C.G.: Combining multisets with integers. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, p. 363. Springer, Heidelberg (2002)"},{"key":"26_CR30","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/11532231_10","volume-title":"Automated Deduction \u2013 CADE-20","author":"T. Zhang","year":"2005","unstructured":"Zhang, T., Sipma, H.B., Manna, Z.: The Decidability of the First-Order Theory of Knuth-Bendix Order. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 131\u2013148. Springer, Heidelberg (2005)"}],"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-642-18275-4_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T23:26:42Z","timestamp":1553383602000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-18275-4_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642182747","9783642182754"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-18275-4_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}