{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:31:19Z","timestamp":1770280279233,"version":"3.49.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319117362","type":"print"},{"value":"9783319117379","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11737-9_18","type":"book-chapter","created":{"date-parts":[[2014,10,15]],"date-time":"2014-10-15T00:52:14Z","timestamp":1413334334000},"page":"267-283","source":"Crossref","is-referenced-by-count":9,"title":["A Resource-Based Logic for Termination and Non-termination Proofs"],"prefix":"10.1007","author":[{"given":"Ton Chanh","family":"Le","sequence":"first","affiliation":[]},{"given":"Cristian","family":"Gherghina","sequence":"additional","affiliation":[]},{"given":"Aquinas","family":"Hobor","sequence":"additional","affiliation":[]},{"given":"Wei-Ngan","family":"Chin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Abel, A.: Type-based termination of generic programs. SCP\u00a074(8) (2009)","DOI":"10.1016\/j.scico.2008.01.004"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., H\u00e4hnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. SSM\u00a04 (2005)","DOI":"10.1007\/s10270-004-0058-x"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-92188-2_5","volume-title":"Formal Methods for Components and Objects","author":"E. Albert","year":"2008","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: COSTA: Design and Implementation of a Cost and Termination Analyzer for Java Bytecode. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol.\u00a05382, pp. 113\u2013132. Springer, Heidelberg (2008)"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W., Momigliano, A.: A program logic for resources. TCS\u00a0389(3) (2007)","DOI":"10.1016\/j.tcs.2007.09.003"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Atkey, R.: Amortised resource analysis with separation logic. LMCS\u00a07(2) (2011)","DOI":"10.2168\/LMCS-7(2:17)2011"},{"key":"18_CR6","unstructured":"Baudin, P., Cuoq, P., Filli\u00e2tre, J.-C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language Version 1.8. (2013), http:\/\/frama-c.com\/acsl.html"},{"key":"18_CR7","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":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1349","DOI":"10.1007\/11523468_109","volume-title":"Automata, Languages and Programming","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: The polyranking principle. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 1349\u20131361. Springer, Heidelberg (2005)"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-642-39799-8_28","volume-title":"Computer Aided Verification","author":"M. Brockschmidt","year":"2013","unstructured":"Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 413\u2013429. Springer, Heidelberg (2013)"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-31762-0_9","volume-title":"Formal Verification of Object-Oriented Software","author":"M. Brockschmidt","year":"2012","unstructured":"Brockschmidt, M., Str\u00f6der, T., Otto, C., Giesl, J.: Automated detection of non-termination and NullPointerExceptions for java bytecode. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol.\u00a07421, pp. 123\u2013141. Springer, Heidelberg (2012)"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Bornat, R., Calcagno, C.: Cyclic proofs of program termination in separation logic. In: POPL (2008)","DOI":"10.1145\/1328438.1328453"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-642-54862-8_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H.-Y. Chen","year":"2014","unstructured":"Chen, H.-Y., Cook, B., Fuhs, C., Nimkar, K., O\u2019Hearn, P.: Proving nontermination via safety. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol.\u00a08413, pp. 156\u2013171. Springer, Heidelberg (2014)"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-70545-1_32","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2008","unstructured":"Cook, B., Gulwani, S., Lev-Ami, T., Rybalchenko, A., Sagiv, M.: Proving conditional termination. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 328\u2013340. Springer, Heidelberg (2008)"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI (2006)","DOI":"10.1145\/1133981.1134029"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P. Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol.\u00a07504, pp. 233\u2013247. Springer, Heidelberg (2012)"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Do, H., Elbaum, S.G., Rothermel, G.: Supporting Controlled Experimentation with Testing Techniques: An Infrastructure and its Potential Impact. In: ESE, vol.\u00a010 (2005)","DOI":"10.1007\/s10664-005-3861-2"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-642-02959-2_22","volume-title":"Automated Deduction \u2013 CADE-22","author":"S. Falke","year":"2009","unstructured":"Falke, S., Kapur, D.: A term rewriting approach to the automated termination analysis of imperative programs. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 277\u2013293. Springer, Heidelberg (2009)"},{"key":"18_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Automated Reasoning","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: aProVE 1.2: automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.: Speed: Precise and efficient static estimation of program computational complexity. In: POPL (2009)","DOI":"10.1145\/1480881.1480898"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.-G.: Proving non-termination. In: POPL (2008)","DOI":"10.1145\/1328438.1328459"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/3-540-51305-1_3","volume-title":"Mathematics of Program Construction","author":"E.C.R. Hehner","year":"1989","unstructured":"Hehner, E.C.R.: Termination is timing. In: van de Snepscheut, J.L.A. (ed.) MPC 1989. LNCS, vol.\u00a0375, pp. 36\u201347. Springer, Heidelberg (1989)"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Hehner, E.C.R.: Specifications, programs, and total correctness. SCP\u00a034(3) (1999)","DOI":"10.1016\/S0167-6423(98)00027-6"},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall (1998)","DOI":"10.1007\/BFb0002714"},{"key":"18_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-11957-6_16","volume-title":"Programming Languages and Systems","author":"J. Hoffmann","year":"2010","unstructured":"Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 287\u2013306. Springer, Heidelberg (2010)"},{"key":"18_CR26","unstructured":"Jones, C.B.: Balancing expressiveness in formal approaches to concurrency (2013)"},{"key":"18_CR27","unstructured":"Kleene, S.: Mathematical logic. Wiley (1967)"},{"key":"18_CR28","doi-asserted-by":"crossref","unstructured":"Le, T.C., Gherghina, C., Hobor, A., Chin, W.-N.: A Resource-Based Logic for Termination and Non-Termination Proofs, Technical Report (2014), http:\/\/loris-7.ddns.comp.nus.edu.sg\/~project\/hiptnt\/HipTNT.pdf","DOI":"10.1007\/978-3-319-11737-9_18"},{"issue":"3","key":"18_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"G.T. Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. SIGSOFT Softw. Eng. Notes\u00a031(3), 1\u201338 (2006)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"18_CR30","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL (2001)","DOI":"10.1145\/360204.360210"},{"key":"18_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"key":"18_CR32","doi-asserted-by":"crossref","unstructured":"Magill, S., Tsai, M.-H., Lee, P., Tsay, Y.-K.: Automatic numeric abstractions for heap-manipulating programs. In: POPL (2010)","DOI":"10.1145\/1706299.1706326"},{"key":"18_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-540-73449-9_23","volume-title":"Term Rewriting and Applications","author":"C. March\u00e9","year":"2007","unstructured":"March\u00e9, C., Zantema, H.: The termination competition. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 303\u2013313. Springer, Heidelberg (2007)"},{"key":"18_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/978-3-642-11957-6_26","volume-title":"Programming Languages and Systems","author":"K. Nakata","year":"2010","unstructured":"Nakata, K., Uustalu, T.: A hoare logic for the coinductive trace-based big-step semantics of while. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 488\u2013506. Springer, Heidelberg (2010)"},{"key":"18_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-540-69738-1_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H.H. Nguyen","year":"2007","unstructured":"Nguyen, H.H., David, C., Qin, S.C., Chin, W.-N.: Automated Verification of Shape and Size Properties Via Separation Logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 251\u2013266. Springer, Heidelberg (2007)"},{"key":"18_CR36","unstructured":"Reynolds, J.: Separation Logic: A Logic for Shared Mutable Data Structures. In: LICS (2002)"},{"key":"18_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-540-79124-9_11","volume-title":"Tests and Proofs","author":"H. Velroyen","year":"2008","unstructured":"Velroyen, H., R\u00fcmmer, P.: Non-termination checking for imperative programs. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol.\u00a04966, pp. 154\u2013170. Springer, Heidelberg (2008)"},{"key":"18_CR38","unstructured":"Xi, H.: Dependent Types for Program Termination Verification. In: LICS (2001)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11737-9_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T04:24:55Z","timestamp":1746419095000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11737-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319117362","9783319117379"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11737-9_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}