{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T08:39:49Z","timestamp":1759826389533},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642140518"},{"type":"electronic","value":"9783642140525"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_25","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"355-370","source":"Crossref","is-referenced-by-count":5,"title":["Interactive Termination Proofs Using Termination Cores"],"prefix":"10.1007","author":[{"given":"Panagiotis","family":"Manolios","sequence":"first","affiliation":[]},{"given":"Daron","family":"Vroon","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1145\/1328438.1328453","volume-title":"POPL \u201908","author":"J. Brotherston","year":"2008","unstructured":"Brotherston, J., Bornat, R., Calcagno, C.: Cyclic proofs of program termination in separation logic. In: POPL \u201908, pp. 101\u2013112. ACM, New York (2008)"},{"key":"25_CR2","unstructured":"Chamarthi, H.R., Dillinger, P.C., Manolios, P., Vroon, D.: ACL2 Sedan homepage, http:\/\/acl2s.ccs.neu.edu\/"},{"key":"25_CR3","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1145\/1133981.1134029","volume-title":"PLDI \u201906","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI \u201906, pp. 415\u2013426. ACM, New York (2006)"},{"issue":"2","key":"25_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2006.09.018","volume":"174","author":"P.C. Dillinger","year":"2007","unstructured":"Dillinger, P.C., Manolios, P., Vroon, D., Strother Moore, J.: ACL2s: \u201cThe ACL2 Sedan\u201d. Electr. Notes Theor. Comput. Sci.\u00a0174(2), 3\u201318 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","year":"2000","key":"25_CR5","unstructured":"Kaufmann, M., Manolios, P., Strother Moore, J. (eds.): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Dordrecht (June 2000)"},{"key":"25_CR6","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Strother Moore, J.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (July 2000)"},{"key":"25_CR7","unstructured":"Kaufmann, M., Strother Moore, J.: ACL2 homepage, http:\/\/www.cs.utexas.edu\/users\/moore\/acl2 (August 2007)"},{"key":"25_CR8","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1145\/360204.360210","volume-title":"POPL \u201901","author":"C.S. Lee","year":"2001","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL \u201901, vol.\u00a028, pp. 81\u201392. ACM, New York (2001)"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/11817963_36","volume-title":"Computer Aided Verification","author":"P. Manolios","year":"2006","unstructured":"Manolios, P., Vroon, D.: Termination analysis with calling context graphs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 401\u2013414. Springer, Heidelberg (2006)"},{"issue":"2-3","key":"25_CR10","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A. Prasad Sistla","year":"1987","unstructured":"Prasad Sistla, A., Vardi, M.Y., Wolper, P.: The complementation problem for b\u00fcchi automata with applications to temporal logic. Theor. Comput. Sci.\u00a049(2-3), 217\u2013237 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Giesl, J.: Size-change termination for term rewriting. Technical Report AIB-2003-02, RWTH Aachen (January 2003)","DOI":"10.1007\/3-540-44881-0_19"},{"key":"25_CR12","first-page":"238","volume-title":"Banff Higher order workshop conference on Logics for concurrency","author":"M.Y. Vardi","year":"1996","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Banff Higher order workshop conference on Logics for concurrency, pp. 238\u2013266. Springer, Heidelberg (1996)"},{"key":"25_CR13","unstructured":"Vroon, D.: Automatically Proving the Termination of Functional Programs. PhD thesis, Georgia Intitute of Technology (2007)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:47:02Z","timestamp":1606186022000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}