{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T04:59:39Z","timestamp":1769749179358,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642317613","type":"print"},{"value":"9783642317620","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31762-0_9","type":"book-chapter","created":{"date-parts":[[2012,7,11]],"date-time":"2012-07-11T10:09:11Z","timestamp":1342001351000},"page":"123-141","source":"Crossref","is-referenced-by-count":32,"title":["Automated Detection of Non-termination and NullPointerExceptions for Java Bytecode"],"prefix":"10.1007","author":[{"given":"Marc","family":"Brockschmidt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Str\u00f6der","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carsten","family":"Otto","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":"9_CR1","unstructured":"http:\/\/aprove.informatik.rwth-aachen.de\/eval\/JBC-Nonterm\/"},{"issue":"5","key":"9_CR2","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1109\/MS.2008.130","volume":"25","author":"N. Ayewah","year":"2008","unstructured":"Ayewah, N., Hovemeyer, D., Morgenthaler, J.D., Penix, J., Pugh, W.: Using static analysis to find bugs. IEEE Software\u00a025(5), 22\u201329 (2008)","journal-title":"IEEE Software"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H.: Verification of Object-Oriented Software: The KeY Approach. LNCS, vol.\u00a04334 (2007)","DOI":"10.1007\/978-3-540-69061-0"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-17172-7_2","volume-title":"Verification, Induction, Termination Analysis","author":"M. Brockschmidt","year":"2010","unstructured":"Brockschmidt, M., Otto, C., von Essen, C., Giesl, J.: Termination Graphs for Java Bytecode. In: Siegler, S., Wasser, N. (eds.) Walther Festschrift. LNCS, vol.\u00a06463, pp. 17\u201337. Springer, Heidelberg (2010); Extended version (with proofs) available [1]"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Str\u00f6der, T., Otto, C., Giesl, J.: Automated detection of non-termination and NullPointerExceptions for Java Bytecode. Report AIB 2011-17, RWTH Aachen, 2011. Available at [1], \n                    \n                      aib.informatik.rwth-aachen.de","DOI":"10.1007\/978-3-642-31762-0_9"},{"key":"9_CR6","unstructured":"Brockschmidt, M., Otto, C., Giesl, J.: Modular termination proofs of recursive Java Bytecode programs by term rewriting. In: Proc. RTA 2011. LIPIcs, vol.\u00a010, pp. 155\u2013170 (2011); Extended version (with proofs) available at [1]"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-17071-3_7","volume-title":"Formal Methods for Components and Objects","author":"R. Bubel","year":"2010","unstructured":"Bubel, R., H\u00e4hnle, R., Ji, R.: Interleaving Symbolic Execution and Partial Evaluation. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol.\u00a06286, pp. 125\u2013146. Springer, Heidelberg (2010)"},{"key":"9_CR8","doi-asserted-by":"crossref","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\u00a0 1977, pp. 238\u2013252. ACM Press (1977)","DOI":"10.1145\/512950.512973"},{"key":"9_CR9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1348250.1348254","volume":"17","author":"C. Csallner","year":"2008","unstructured":"Csallner, C., Smaragdakis, Y., Xie, T.: DSD-Crasher: A hybrid analysis tool for bug finding. ACM Trans. Softw. Eng. Methodol.\u00a017, 8:1\u20138:37 (2008)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"9_CR10","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.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"9_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/11559306_12","volume-title":"Frontiers of Combining Systems","author":"J. Giesl","year":"2005","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and Disproving Termination of Higher-Order Functions. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol.\u00a03717, pp. 216\u2013231. Springer, Heidelberg (2005)"},{"key":"9_CR12","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":"9_CR13","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: Proc. PLDI 2005, pp. 213\u2013223. ACM Press (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.: Proving non-termination. In: Proc. POPL\u00a02008, pp. 147\u2013158. ACM Press (2008)","DOI":"10.1145\/1328897.1328459"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-540-68863-1_9","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"L. Hubert","year":"2008","unstructured":"Hubert, L., Jensen, T., Pichardie, D.: Semantic Foundations and Inference of Non-null Annotations. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol.\u00a05051, pp. 132\u2013149. Springer, Heidelberg (2008)"},{"key":"9_CR16","unstructured":"Lindholm, T., Yellin, F.: Java Virtual Machine Specification. Prentice Hall (1999)"},{"key":"9_CR17","unstructured":"Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: Proc. RTA\u00a02010. LIPIcs, vol.\u00a06, pp. 259\u2013276 (2010); Extended version (with proofs) available at [1]"},{"key":"9_CR18","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/1119479.1119481","volume":"28","author":"\u00c9. Payet","year":"2006","unstructured":"Payet, \u00c9., Mesnard, F.: Nontermination inference of logic programs. ACM Trans. Prog. Lang. Syst.\u00a028, 256\u2013289 (2006)","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"9_CR19","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/j.tcs.2008.05.013","volume":"403","author":"\u00c9. Payet","year":"2008","unstructured":"Payet, \u00c9.: Loop detection in term rewriting using the eliminating unfoldings. Theoretical Computer Science\u00a0403, 307\u2013327 (2008)","journal-title":"Theoretical Computer Science"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Payet, \u00c9., Spoto, F.: Experiments with non-termination analysis for Java Bytecode. In: Proc. BYTECODE 2009. ENTCS, vol.\u00a05, pp. 83\u201396 (2009)","DOI":"10.1016\/j.entcs.2009.11.016"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: A concolic unit testing engine for C. In: Proc. FSE\u00a0 2010, pp. 263\u2013272. ACM Press (2005)","DOI":"10.21236\/ADA482657"},{"key":"9_CR22","unstructured":"S\u00f8rensen, M.H., Gl\u00fcck, R.: An algorithm of generalization in positive supercompilation. In: Proc. ILPS\u00a0 1995, pp. 465\u2013479. MIT Press (1995)"},{"key":"9_CR23","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10270-009-0132-5","volume":"10","author":"F. Spoto","year":"2011","unstructured":"Spoto, F.: Precise null-pointer analysis. Softw. Syst. Model.\u00a010, 219\u2013252 (2011)","journal-title":"Softw. Syst. Model."},{"key":"9_CR24","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":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-70545-1_36","volume-title":"Computer Aided Verification","author":"H. Yang","year":"2008","unstructured":"Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.: Scalable Shape Analysis for Systems Code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 385\u2013398. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Formal Verification of Object-Oriented Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31762-0_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:47:38Z","timestamp":1620128858000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31762-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642317613","9783642317620"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31762-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}