{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:32:43Z","timestamp":1725568363201},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642171710"},{"type":"electronic","value":"9783642171727"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-17172-7_2","type":"book-chapter","created":{"date-parts":[[2010,11,2]],"date-time":"2010-11-02T13:17:15Z","timestamp":1288703835000},"page":"17-37","source":"Crossref","is-referenced-by-count":25,"title":["Termination Graphs for Java Bytecode"],"prefix":"10.1007","author":[{"given":"Marc","family":"Brockschmidt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carsten","family":"Otto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"von Essen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-68863-1_2","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"E. Albert","year":"2008","unstructured":"Albert, E., Arenas, P., Codish, M., Genaim, S., Puebla, G., Zanardini, D.: Termination analysis of Java Bytecode. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol.\u00a05051, pp. 2\u201318. Springer, Heidelberg (2008)"},{"key":"2_CR2","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.: 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":"2_CR3","doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Otto, C., von Essen, C., Giesl, J.: Termination graphs for Java Bytecode. Technical Report AIB-2010-15, RWTH Aachen (2010), http:\/\/aib.informatik.rwth-aachen.de","DOI":"10.1007\/978-3-642-17172-7_2"},{"key":"2_CR4","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. Col\u00f3n","year":"2002","unstructured":"Col\u00f3n, 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":"2_CR5","first-page":"415","volume-title":"PLDI 2006","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Schwartzbach, M.I., Ball, T. (eds.) PLDI 2006, pp. 415\u2013426. ACM Press, New York (2006)"},{"key":"2_CR6","first-page":"238","volume-title":"Proc. POPL\u00a01977","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. POPL\u00a01977, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"2_CR7","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/0743-1066(94)90027-2","volume":"19-20","author":"D. Schreye De","year":"1994","unstructured":"De Schreye, D., Decorte, S.: Termination of logic programs: The never-ending story. Journal of Logic Programming\u00a019-20, 199\u2013260 (1994)","journal-title":"Journal of Logic Programming"},{"issue":"1-2","key":"2_CR8","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"Dershowitz, N.: Termination of rewriting. J. Symb. Comp.\u00a03(1-2), 69\u2013116 (1987)","journal-title":"J. Symb. Comp."},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-02348-4_3","volume-title":"Rewriting Techniques and Applications","author":"C. Fuhs","year":"2009","unstructured":"Fuhs, C., Giesl, J., Pl\u00fccker, M., Schneider-Kamp, P., Falke, S.: Proving termination of integer term rewriting. In: Treinen, R. (ed.) RTA 2009. LNCS, vol.\u00a05595, pp. 32\u201347. Springer, Heidelberg (2009)"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for Haskell by term rewriting. ACM TOPLAS (to appear)","DOI":"10.1145\/1890028.1890030"},{"key":"2_CR11","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 DP framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"issue":"4","key":"2_CR12","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G. Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM TOPLAS\u00a028(4), 619\u2013695 (2006)","journal-title":"ACM TOPLAS"},{"key":"2_CR13","volume-title":"Java Virtual Machine Specification","author":"T. Lindholm","year":"1999","unstructured":"Lindholm, T., Yellin, F.: Java Virtual Machine Specification. Prentice-Hall, Englewood Cliffs (1999)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: Lynch, C. (ed.) RTA 2010. LIPIcs, vol.\u00a06, pp. 259\u2013276. Dagstuhl Publishing (2010)","DOI":"10.1007\/978-3-642-17172-7_2"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Schneider-Kamp, P., Giesl, J., Serebrenik, A., Thiemann, R.: Automated termination proofs for logic programs by term rewriting. ACM TOCL\u00a011(1) (2009)","DOI":"10.1145\/1614431.1614433"},{"key":"2_CR17","first-page":"465","volume-title":"ILPS 1995","author":"M.H. S\u00f8rensen","year":"1995","unstructured":"S\u00f8rensen, M.H., Gl\u00fcck, R.: An algorithm of generalization in positive supercompilation. In: Lloyd, J.W. (ed.) ILPS 1995, pp. 465\u2013479. MIT Press, Cambridge (1995)"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Spoto, F., Mesnard, F., Payet, \u00c9.: A termination analyser for Java Bytecode based on path-length. ACM TOPLAS\u00a032(3) (2010)","DOI":"10.1145\/1709093.1709095"},{"key":"2_CR19","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1093\/oso\/9780198537465.003.0003","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"C. Walther","year":"1994","unstructured":"Walther, C.: Mathematical induction. In: Handbook of Logic in Artificial Intelligence and Logic Programming, vol.\u00a02, pp. 127\u2013227. Oxford University Press, Oxford (1994)"},{"issue":"1","key":"2_CR20","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/0004-3702(94)90063-9","volume":"71","author":"C. Walther","year":"1994","unstructured":"Walther, C.: On proving the termination of algorithms by machine. Artificial Intelligence\u00a071(1), 101\u2013157 (1994)","journal-title":"Artificial Intelligence"},{"key":"2_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-322-86768-1","volume-title":"Semantik und Programmverifikation","author":"C. Walther","year":"2001","unstructured":"Walther, C.: Semantik und Programmverifikation. Teubner-Wiley, Chichester (2001)"}],"container-title":["Lecture Notes in Computer Science","Verification, Induction, Termination Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17172-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,31]],"date-time":"2024-03-31T23:00:00Z","timestamp":1711926000000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17172-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642171710","9783642171727"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17172-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}