{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T16:19:33Z","timestamp":1762273173400,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031477041"},{"type":"electronic","value":"9783031477058"}],"license":[{"start":{"date-parts":[[2023,11,6]],"date-time":"2023-11-06T00:00:00Z","timestamp":1699228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,11,6]],"date-time":"2023-11-06T00:00:00Z","timestamp":1699228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-47705-8_7","type":"book-chapter","created":{"date-parts":[[2023,11,10]],"date-time":"2023-11-10T09:02:24Z","timestamp":1699606944000},"page":"113-133","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Reasoning About Exceptional Behavior at\u00a0the\u00a0Level of\u00a0Java Bytecode"],"prefix":"10.1007","author":[{"given":"Marco","family":"Paganoni","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1040-3201","authenticated-orcid":false,"given":"Carlo A.","family":"Furia","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,11,6]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., et al.: The KeY platform for verification and analysis of java programs. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 55\u201371. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12154-3_4","DOI":"10.1007\/978-3-319-12154-3_4"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Banerjee, S., Clapp, L., Sridharan, M.: NullAway: practical type-based null safety for Java. In: Dumas, M., Pfahl, D., Apel, S., Russo, A. (eds.) Proceedings of the ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/SIGSOFT FSE 2019, Tallinn, Estonia, 26\u201330 August 2019, pp. 740\u2013750. ACM (2019). https:\/\/doi.org\/10.1145\/3338906.3338919","DOI":"10.1145\/3338906.3338919"},{"key":"7_CR3","doi-asserted-by":"publisher","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_17","DOI":"10.1007\/11804192_17"},{"key":"7_CR4","doi-asserted-by":"publisher","unstructured":"Calcagno, C., et al.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3\u201311. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_1","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Chrz\u0105szcz, J., Huisman, M., Schubert, A.: BML and related tools. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol. 5751, pp. 278\u2013297. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04167-9_14","DOI":"10.1007\/978-3-642-04167-9_14"},{"key":"7_CR6","doi-asserted-by":"publisher","unstructured":"Cok, D.R.: OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse. In: Dubois, C., Giannakopoulou, D., M\u00e9ry, D. (eds.) Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, Grenoble, 6 April 2014. EPTCS, 149, pp. 79\u201392 (2014). https:\/\/doi.org\/10.4204\/EPTCS.149.8","DOI":"10.4204\/EPTCS.149.8"},{"key":"7_CR7","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173\u2013177. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_21","DOI":"10.1007\/978-3-540-73368-3_21"},{"key":"7_CR8","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Hiep, H.A., Maathuis, O., Bian, J., de Boer, F.S., de Gouw, S.: Verifying OpenJDK\u2019s LinkedList using KeY (extended paper). Int. J. Softw. Tools Technol. Transf. 24(5), 783\u2013802 (2022). https:\/\/doi.org\/10.1007\/s10009-022-00679-7","DOI":"10.1007\/s10009-022-00679-7"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Kahsai, T., R\u00fcmmer, P., Sanchez, H., Sch\u00e4f, M.: JayHorn: a framework for verifying Java programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 352\u2013358. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_19","DOI":"10.1007\/978-3-319-41528-4_19"},{"key":"7_CR11","unstructured":"Lam, P., Bodden, E., Lhot\u00e1k, O., Hendren, L.: The Soot framework for Java program analysis: a retrospective. In: Cetus Users and Compiler Infrastructure Workshop (CETUS 2011) (2011). https:\/\/www.bodden.de\/pubs\/lblh11soot.pdf"},{"key":"7_CR12","doi-asserted-by":"publisher","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The KRAKATOA tool for certification of JAVA\/JAVACARD programs annotated in JML. J. Log. Algeb. Methods Prog. 58(1\u20132), 89\u2013106 (2004). https:\/\/doi.org\/10.1016\/j.jlap.2003.07.006","DOI":"10.1016\/j.jlap.2003.07.006"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Marcilio, D., Furia, C.A.: How Java programmers test exceptional behavior. In: Proceedings of the 18th Mining Software Repositories Conference (MSR), pp. 207\u2013218. IEEE (2021)","DOI":"10.1109\/MSR52588.2021.00033"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Marcilio, D., Furia, C.A.: What is thrown? Lightweight precise automatic extraction of exception preconditions in Java methods. In: Proceedings of the 38th IEEE International Conference on Software Maintenance and Evolution (ICSME), pp. 340\u2013351. IEEE Computer Society (2022)","DOI":"10.1109\/ICSME55016.2022.00038"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Melo, H., Coelho, R., Treude, C.: Unveiling exception handling guidelines adopted by Java developers. In: SANER. IEEE (2019)","DOI":"10.1109\/SANER.2019.8668001"},{"key":"7_CR16","doi-asserted-by":"publisher","unstructured":"M\u00fcller, P., Nordio, M.: Proof-transforming compilation of programs with abrupt termination. In: Proceedings of SAVCBS, pp. 39\u201346. ACM (2007). https:\/\/doi.org\/10.1145\/1292316.1292321","DOI":"10.1145\/1292316.1292321"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Nakshatri, S., Hegde, M., Thandra, S.: Analysis of exception handling patterns in Java projects: An empirical study. IEEE\/ACM MSR (2016)","DOI":"10.1145\/2901739.2903499"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Necula, G.C.: Proof-carrying code. In: Lee, P., Henglein, F., Jones, N.D. (eds.) POPL, pp. 106\u2013119. ACM Press (1997). https:\/\/doi.org\/10.1145\/263699.263712","DOI":"10.1145\/263699.263712"},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"Paganoni, M., Furia, C.A.: ByteBack iFM 2023 Replication Package (2023). https:\/\/doi.org\/10.5281\/zenodo.8335240","DOI":"10.5281\/zenodo.8335240"},{"key":"7_CR20","doi-asserted-by":"publisher","unstructured":"Paganoni, M., Furia, C.A.: Verifying functional correctness properties at the level of Java bytecode. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) Proceedings of the 25th International Symposium on Formal Methods (FM). LNCS, vol. 14000, pp. 343\u2013363. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_20","DOI":"10.1007\/978-3-031-27481-7_20"},{"key":"7_CR21","doi-asserted-by":"publisher","unstructured":"Papi, M.M., Ali, M., Jr., T.L.C., Perkins, J.H., Ernst, M.D.: Practical pluggable types for Java. In: Ryder, B.G., Zeller, A. (eds.) Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2008, Seattle, 20\u201324 July 2008, pp. 201\u2013212. ACM (2008). https:\/\/doi.org\/10.1145\/1390630.1390656","DOI":"10.1145\/1390630.1390656"},{"issue":"5","key":"7_CR22","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/s00165-017-0435-1","volume":"30","author":"N Polikarpova","year":"2018","unstructured":"Polikarpova, N., Tschannen, J., Furia, C.A.: A fully verified container library. Formal Aspects Comput. 30(5), 495\u2013523 (2018)","journal-title":"Formal Aspects Comput."},{"key":"7_CR23","doi-asserted-by":"publisher","unstructured":"Rakamari\u0107, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 106\u2013113. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_7","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"7_CR24","doi-asserted-by":"publisher","unstructured":"Rudich, A., Darvas, \u00c1., M\u00fcller, P.: Checking well-formedness of pure-method specifications. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 68\u201383. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68237-0_7","DOI":"10.1007\/978-3-540-68237-0_7"},{"key":"7_CR25","doi-asserted-by":"publisher","unstructured":"R\u00fcmmer, P.: JayHorn: a Java model checker. In: Murray, T., Ernst, G. (eds.) Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs, FTfJP@ECOOP 2019, London, 15 July 2019, p. 1:1. ACM (2019). https:\/\/doi.org\/10.1145\/3340672.3341113","DOI":"10.1145\/3340672.3341113"},{"key":"7_CR26","unstructured":"Vall\u00e9e-Rai, R., Co, P., Gagnon, E., Hendren, L.J., Lam, P., Sundaresan, V.: Soot - a Java bytecode optimization framework. In: MacKay, S.A., Johnson, J.H. (eds.) Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research, 8\u201311 November 1999, Mississauga, p. 13. IBM (1999). https:\/\/dl.acm.org\/citation.cfm?id=782008"},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"Weimer, W., Necula, G.C.: Finding and preventing run-time error handling mistakes. In: Proceedings of the 19th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2004 (October), pp. 24\u201328, 2004. Vancouver, BC, Canada, pp. 419\u2013431. ACM (2004). https:\/\/doi.org\/10.1145\/1028976.1029011","DOI":"10.1145\/1028976.1029011"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-47705-8_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,18]],"date-time":"2024-04-18T14:52:06Z","timestamp":1713451926000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-47705-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,6]]},"ISBN":["9783031477041","9783031477058"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-47705-8_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023,11,6]]},"assertion":[{"value":"6 November 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"iFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Leiden","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 November 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 November 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/liacs.leidenuniv.nl\/~bonsanguemm\/ifm23\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"51","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}