{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T13:28:15Z","timestamp":1762262895202,"version":"build-2065373602"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"4","funder":[{"name":"SNF","award":["200021-207919"],"award-info":[{"award-number":["200021-207919"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,12,31]]},"abstract":"<jats:p>A program\u2019s exceptional behavior can substantially complicate its control flow, and hence accurately reasoning about the program\u2019s correctness. On the other hand, formally verifying realistic programs is likely to involve exceptions\u2014a ubiquitous feature in modern programming languages.<\/jats:p>\n                  <jats:p>\n                    In this article, we present a novel approach to verify the exceptional behavior of Java programs, which extends our previous work on\n                    <jats:sc>ByteBack<\/jats:sc>\n                    .\n                    <jats:sc>ByteBack<\/jats:sc>\n                    works on a program\u2019s bytecode, while providing means to specify the intended behavior at the source-code level; this approach sets\n                    <jats:sc>ByteBack<\/jats:sc>\n                    apart from most state-of-the-art verifiers that target source code. To explicitly model a program\u2019s exceptional behavior in a way that is amenable to formal reasoning, we introduce Vimp: a high-level bytecode representation that extends the Soot framework\u2019s Jimple with verification-oriented features, thus serving as an intermediate layer between bytecode and the Boogie intermediate verification language. Working on bytecode through this intermediate layer brings flexibility and adaptability to new language versions and variants: as our experiments demonstrate,\n                    <jats:sc>ByteBack<\/jats:sc>\n                    can verify programs involving exceptional behavior in all versions of Java, as well as in Scala and Kotlin (two other popular JVM languages).\n                  <\/jats:p>","DOI":"10.1145\/3712015","type":"journal-article","created":{"date-parts":[[2025,1,13]],"date-time":"2025-01-13T06:33:31Z","timestamp":1736750011000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Reasoning About Exceptional Behavior At the Level of Java Bytecode with ByteBack"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-8511-7111","authenticated-orcid":false,"given":"Marco","family":"Paganoni","sequence":"first","affiliation":[{"name":"Universit\u00e0 della Svizzera italiana","place":["Lugano, Switzerland"]}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1040-3201","authenticated-orcid":false,"given":"Carlo A.","family":"Furia","sequence":"additional","affiliation":[{"name":"Universit\u00e0 della Svizzera italiana","place":["Lugano, Switzerland"]}]}],"member":"320","published-online":{"date-parts":[[2025,11,4]]},"reference":[{"key":"e_1_3_2_2_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/978-3-319-12154-3_4","volume-title":"Proceedings of the 6th International Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2014, Vienna, Austria, July 17\u201318, 2014, Revised Selected Papers","volume":"8471","author":"Ahrendt Wolfgang","year":"2014","unstructured":"Wolfgang Ahrendt, Bernhard Beckert, Daniel Bruns, Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner H\u00e4hnle, Martin Hentschel, Mihai Herda, Vladimir Klebanov, et al.2014. The KeY platform for verification and analysis of Java programs. In Proceedings of the 6th International Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2014, Vienna, Austria, July 17\u201318, 2014, Revised Selected Papers, Dimitra Giannakopoulou and Daniel Kroening (Eds.). Lecture Notes in Computer Science, Vol. 8471, Springer, 55\u201371. DOI:DOI:10.1007\/978-3-319-12154-3_4"},{"key":"e_1_3_2_3_2","first-page":"740","volume-title":"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, August 26\u201330, 2019","author":"Banerjee Subarno","year":"2019","unstructured":"Subarno Banerjee, Lazaro Clapp, and Manu Sridharan. 2019. NullAway: Practical type-based null safety for Java. In 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, August 26\u201330, 2019, Marlon Dumas, Dietmar Pfahl, Sven Apel, and Alessandra Russo (Eds.). ACM, 740\u2013750. DOI:DOI:10.1145\/3338906.3338919"},{"key":"e_1_3_2_4_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Proceedings of the 4th International Symposium on Formal Methods for Components and Objects, FMCO 2005, Amsterdam, The Netherlands, November 1\u20134, 2005, Revised Lectures","volume":"4111","author":"Barnett Michael","year":"2005","unstructured":"Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005. Boogie: A modular reusable verifier for object-oriented P rograms. In Proceedings of the 4th International Symposium on Formal Methods for Components and Objects, FMCO 2005, Amsterdam, The Netherlands, November 1\u20134, 2005, Revised Lectures, Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever (Eds.). Lecture Notes in Computer Science, Vol. 4111, Springer, 364\u2013387. DOI:DOI:10.1007\/11804192_17"},{"key":"e_1_3_2_5_2","article-title":"Verification of object-oriented programs with invariants","volume":"3","author":"Barnett Mike","year":"2004","unstructured":"Mike Barnett, Robert DeLine, Manuel F\u00e4hndrich, K. Rustan M. Leino, and Wolfram Schulte. 2004. Verification of object-oriented programs with invariants. Journal of Object Technology 3, 6 (2004), 27\u201356.","journal-title":"Journal of Object Technology"},{"key":"e_1_3_2_6_2","first-page":"54","volume-title":"Proceedings of the MPC","author":"Barnett Michael","year":"2004","unstructured":"Michael Barnett and David A. Naumann. 2004. Friends need a bit more: Maintaining invariants over shared state. In Proceedings of the MPC. 54\u201384."},{"key":"e_1_3_2_7_2","first-page":"227","volume-title":"Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2008, October 19\u201323, 2008, Nashville, TN, USA","author":"Beckman Nels E.","year":"2008","unstructured":"Nels E. Beckman, Kevin Bierhoff, and Jonathan Aldrich. 2008. Verifying correct usage of atomic blocks and typestate. In Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2008, October 19\u201323, 2008, Nashville, TN, USA. ACM, 227\u2013244. DOI:DOI:10.1145\/1449764.1449783"},{"key":"e_1_3_2_8_2","first-page":"475","volume-title":"Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2008, October 19\u201323, 2008, Nashville, TN, USA","author":"Bellamy Ben","year":"2008","unstructured":"Ben Bellamy, Pavel Avgustinov, Oege de Moor, and Damien Sereni. 2008. Efficient local type inference. In Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2008, October 19\u201323, 2008, Nashville, TN, USA, Gail E. Harris (Ed.). ACM, 475\u2013492. DOI:DOI:10.1145\/1449764.1449802"},{"key":"e_1_3_2_9_2","first-page":"301","volume-title":"Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007, October 21\u201325, 2007, Montreal, Quebec, Canada","author":"Bierhoff Kevin","year":"2007","unstructured":"Kevin Bierhoff and Jonathan Aldrich. 2007. Modular typestate checking of aliased objects. In Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007, October 21\u201325, 2007, Montreal, Quebec, Canada. ACM, 301\u2013320. DOI:DOI:10.1145\/1297027.1297050"},{"key":"e_1_3_2_10_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/978-3-319-06410-9_9","volume-title":"Proceedings of the 19th International Symposium on Formal Methods, FM 2014, Singapore, May 12\u201316, 2014","volume":"8442","author":"Blom Stefan","year":"2014","unstructured":"Stefan Blom and Marieke Huisman. 2014. The VerCors tool for verification of concurrent programs. In Proceedings of the 19th International Symposium on Formal Methods, FM 2014, Singapore, May 12\u201316, 2014, Cliff B. Jones, Pekka Pihlajasaari, and Jun Sun (Eds.). Lecture Notes in Computer Science, Vol. 8442, Springer, 127\u2013131. DOI:DOI:10.1007\/978-3-319-06410-9_9"},{"key":"e_1_3_2_11_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-319-17524-9_1","volume-title":"Proceedings of the 7th International Symposium on NASA Formal Methods, NFM 2015, Pasadena, CA, USA, April 27\u201329, 2015","volume":"9058","author":"Calcagno Cristiano","year":"2015","unstructured":"Cristiano Calcagno, Dino Distefano, J\u00e9r\u00e9my Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter W. O\u2019Hearn, Irene Papakonstantinou, Jim Purbrick, and Dulma Rodriguez. 2015. Moving fast with software verification. In Proceedings of the 7th International Symposium on NASA Formal Methods, NFM 2015, Pasadena, CA, USA, April 27\u201329, 2015, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi (Eds.). Lecture Notes in Computer Science, Vol. 9058, Springer, 3\u201311. DOI:DOI:10.1007\/978-3-319-17524-9_1"},{"key":"e_1_3_2_12_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1007\/978-3-642-04167-9_14","volume-title":"Proceedings of the 7th International Symposium on Formal Methods for Components and Objects, FMCO 2008, Sophia Antipolis, France, October 21\u201323, 2008, Revised Lectures","volume":"5751","author":"Chrzaszcz Jacek","year":"2008","unstructured":"Jacek Chrzaszcz, Marieke Huisman, and Aleksy Schubert. 2008. BML and related tools. In Proceedings of the 7th International Symposium on Formal Methods for Components and Objects, FMCO 2008, Sophia Antipolis, France, October 21\u201323, 2008, Revised Lectures, Frank S. de Boer, Marcello M. Bonsangue, and Eric Madelaine (Eds.). Lecture Notes in Computer Science, Vol. 5751, Springer, 278\u2013297. DOI:DOI:10.1007\/978-3-642-04167-9_14"},{"key":"e_1_3_2_13_2","first-page":"480","volume-title":"Proceedings of the CAV (Lecture Notes in Computer Science)","author":"Cohen Ernie","year":"2010","unstructured":"Ernie Cohen, Michal Moskal, Wolfram Schulte, and Stephan Tobies. 2010. Local verification of global invariants in concurrent programs. In Proceedings of the CAV (Lecture Notes in Computer Science). Springer, 480\u2013494."},{"key":"e_1_3_2_14_2","first-page":"79","volume-title":"Proceedings of the 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, Grenoble, France, April 6, 2014 (EPTCS)","volume":"149","author":"Cok David R.","year":"2014","unstructured":"David R. Cok. 2014. OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse. In Proceedings of the 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, Grenoble, France, April 6, 2014 (EPTCS), Catherine Dubois, Dimitra Giannakopoulou, and Dominique M\u00e9ry (Eds.). Vol. 149, 79\u201392. DOI:DOI:10.4204\/EPTCS.149.8"},{"key":"e_1_3_2_15_2","first-page":"412","volume-title":"Proceedings of the 22nd European Conference on Object-Oriented Programming, ECOOP 2008, , Paphos, Cyprus, July 7\u201311, 2008.","author":"Drossopoulou Sophia","year":"2008","unstructured":"Sophia Drossopoulou, Adrian Francalanza, Peter M\u00fcller, and Alexander J. Summers. 2008. A unified framework for verification techniques for object invariants. In Proceedings of the 22nd European Conference on Object-Oriented Programming, ECOOP 2008, , Paphos, Cyprus, July 7\u201311, 2008. . Springer, 412\u2013437. DOI:DOI:10.1007\/978-3-540-70592-5_18"},{"key":"e_1_3_2_16_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification, CAV 2007, Berlin, Germany, July 3\u20137, 2007","volume":"4590","author":"Filli\u00e2tre Jean-Christophe","year":"2007","unstructured":"Jean-Christophe Filli\u00e2tre and Claude March\u00e9. 2007. The Why\/Krakatoa\/Caduceus platform for deductive program verification. In Proceedings of the 19th International Conference on Computer Aided Verification, CAV 2007, Berlin, Germany, July 3\u20137, 2007, Werner Damm and Holger Hermanns (Eds.). Lecture Notes in Computer Science, Vol. 4590, Springer, 173\u2013177. DOI:DOI:10.1007\/978-3-540-73368-3_21"},{"key":"e_1_3_2_17_2","first-page":"125","volume-title":"Proceedings of the Programming Languages and Systems\u201422nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16\u201324, 2013.","author":"Filli\u00e2tre Jean-Christophe","year":"2013","unstructured":"Jean-Christophe Filli\u00e2tre and Andrei Paskevich. 2013. Why3 - where programs meet provers. In Proceedings of the Programming Languages and Systems\u201422nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16\u201324, 2013.Springer, 125\u2013128. DOI:DOI:10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_18_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Proceedings of the 27th International Conference on Computer Aided Verification, CAV 2015, San Francisco, CA, USA, July 18\u201324, 2015, Part I","volume":"9206","author":"Gurfinkel Arie","year":"2015","unstructured":"Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn verification framework. In Proceedings of the 27th International Conference on Computer Aided Verification, CAV 2015, San Francisco, CA, USA, July 18\u201324, 2015, Part I, Daniel Kroening and Corina S. Pasareanu (Eds.). Lecture Notes in Computer Science, Vol. 9206, Springer, 343\u2013361. DOI:DOI:10.1007\/978-3-319-21690-4_20"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-022-00679-7"},{"key":"e_1_3_2_20_2","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"Proceedings of the 3rd International Symposium on NASA Formal Methods, NFM 2011, Pasadena, CA, USA, April 18\u201320, 2011.","author":"Jacobs Bart","year":"2011","unstructured":"Bart Jacobs, Jan Smans, Pieter Philippaerts, Fr\u00e9d\u00e9ric Vogels, Willem Penninckx, and Frank Piessens. 2011. VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In Proceedings of the 3rd International Symposium on NASA Formal Methods, NFM 2011, Pasadena, CA, USA, April 18\u201320, 2011.Springer, 41\u201355. DOI:DOI:10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_2_21_2","first-page":"304","volume-title":"Proceedings of the 8th Asian Symposium on Programming Languages and Systems, APLAS 2010, Shanghai, China, November 28\u2013December 1, 2010.","author":"Jacobs Bart","year":"2010","unstructured":"Bart Jacobs, Jan Smans, and Frank Piessens. 2010. A quick tour of the VeriFast program verifier. In Proceedings of the 8th Asian Symposium on Programming Languages and Systems, APLAS 2010, Shanghai, China, November 28\u2013December 1, 2010.Springer, 304\u2013311. DOI:DOI:10.1007\/978-3-642-17164-2_21"},{"key":"e_1_3_2_22_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1007\/978-3-319-41528-4_19","volume-title":"Proceedings of the 28th International Conference on Computer Aided Verification, CAV 2016, Toronto, ON, Canada, July 17\u201323, 2016, Part I","volume":"9779","author":"Kahsai Temesghen","year":"2016","unstructured":"Temesghen Kahsai, Philipp R\u00fcmmer, Huascar Sanchez, and Martin Sch\u00e4f. 2016. JayHorn: A framework for verifying Java programs. In Proceedings of the 28th International Conference on Computer Aided Verification, CAV 2016, Toronto, ON, Canada, July 17\u201323, 2016, Part I, Swarat Chaudhuri and Azadeh Farzan (Eds.). Lecture Notes in Computer Science, Vol. 9779, Springer, 352\u2013358. DOI:DOI:10.1007\/978-3-319-41528-4_19"},{"key":"e_1_3_2_23_2","volume-title":"Proceedings of the Cetus Users and Compiler Infrastructure Workshop (CETUS\u201911)","author":"Lam Patrick","year":"2011","unstructured":"Patrick Lam, Eric Bodden, Ond\u0159ej Lhot\u00e1k, and Laurie Hendren. 2011. The Soot framework for Java program analysis: A retrospective. In Proceedings of the Cetus Users and Compiler Infrastructure Workshop (CETUS\u201911). Retrieved from https:\/\/www.bodden.de\/pubs\/lblh11soot.pdf"},{"key":"e_1_3_2_24_2","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Proceedings of the Behavioral Specifications of Businesses and Systems","author":"Leavens Gary T.","year":"1999","unstructured":"Gary T. Leavens, Albert L. Baker, and Clyde Ruby. 1999. JML: A notation for detailed design. In Proceedings of the Behavioral Specifications of Businesses and Systems. Springer, 175\u2013188."},{"key":"e_1_3_2_25_2","first-page":"491","volume-title":"Proceedings of the ECOOP (Lecture Notes in Computer Science)","author":"Leino K. Rustan M.","year":"2004","unstructured":"K. Rustan M. Leino and Peter M\u00fcller. 2004. Object invariants in dynamic contexts. In Proceedings of the ECOOP (Lecture Notes in Computer Science). Springer, 491\u2013516."},{"key":"e_1_3_2_26_2","first-page":"80","volume-title":"Proceedings of the ESOP (Lecture Notes in Computer Science)","author":"Leino K. Rustan M.","year":"2007","unstructured":"K. Rustan M. Leino and Wolfram Schulte. 2007. Using history invariants to verify observers. In Proceedings of the ESOP (Lecture Notes in Computer Science). Springer, 80\u201394."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2003.07.006"},{"key":"e_1_3_2_28_2","first-page":"207","volume-title":"Proceedings of the 18th Mining Software Repositories Conference (MSR\u201921)","author":"Marcilio Diego","year":"2021","unstructured":"Diego Marcilio and Carlo A. Furia. 2021. How Java programmers test exceptional behavior. In Proceedings of the 18th Mining Software Repositories Conference (MSR\u201921). IEEE, 207\u2013218."},{"key":"e_1_3_2_29_2","first-page":"340","volume-title":"Proceedings of the 38th IEEE International Conference on Software Maintenance and Evolution (ICSME\u201922)","author":"Marcilio Diego","year":"2022","unstructured":"Diego Marcilio and Carlo A. Furia. 2022. 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\u201922). IEEE Computer Society, 340\u2013351."},{"key":"e_1_3_2_30_2","volume-title":"Proceedings of the SANER","author":"Melo Hugo","year":"2019","unstructured":"Hugo Melo, Roberta Coelho, and Christoph Treude. 2019. Unveiling exception handling guidelines adopted by Java developers. In Proceedings of the SANER. IEEE."},{"key":"e_1_3_2_31_2","first-page":"40:1\u201340:29","volume-title":"Proceedings of the 37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17\u201321, 2023, Seattle, Washington, United States (LIPIcs)","author":"Mota Jo\u00e3o","year":"2023","unstructured":"Jo\u00e3o Mota, Marco Giunti, and Ant\u00f3nio Ravara. 2023. On using VeriFast, VerCors, Plural, and KeY to check object usage (experience paper). In Proceedings of the 37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17\u201321, 2023, Seattle, Washington, United States (LIPIcs). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 40:1\u201340:29. DOI:DOI:10.4230\/LIPICS.ECOOP.2023.40"},{"key":"e_1_3_2_32_2","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1145\/1292316.1292321","volume-title":"Proceedings of the SAVCBS","author":"M\u00fcller Peter","year":"2007","unstructured":"Peter M\u00fcller and Martin Nordio. 2007. Proof-transforming compilation of programs with abrupt termination. In Proceedings of the SAVCBS. ACM, 39\u201346. DOI:10.1145\/1292316.1292321"},{"issue":"3","key":"e_1_3_2_33_2","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/j.scico.2006.03.001","article-title":"Modular invariants for layered object structures","volume":"62","author":"M\u00fcller Peter","year":"2006","unstructured":"Peter M\u00fcller, Arnd Poetzsch-Heffter, and Gary T. Leavens. 2006. Modular invariants for layered object structures. Science of Computer Programming 62, 3 (2006), 253\u2013286.","journal-title":"Science of Computer Programming"},{"key":"e_1_3_2_34_2","article-title":"Analysis of exception handling patterns in Java projects: An empirical study","author":"Nakshatri Suman","year":"2016","unstructured":"Suman Nakshatri, Maithri Hegde, and Sahithi Thandra. 2016. Analysis of exception handling patterns in Java projects: An empirical study. IEEE\/ACM MSR (2016).","journal-title":"IEEE\/ACM MSR"},{"key":"e_1_3_2_35_2","first-page":"106","volume-title":"Proceedings of the POPL","author":"Necula George C.","year":"1997","unstructured":"George C. Necula. 1997. Proof-carrying code. In Proceedings of the POPL, Peter Lee, Fritz Henglein, and Neil D. Jones (Eds.). ACM,106\u2013119. DOI:DOI:10.1145\/263699.263712"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","unstructured":"Marco Paganoni and Carlo A. Furia. 2024. ByteBack: Replication Package for FAC 2024. DOI:10.6084\/m9.figshare.26491456.v5","DOI":"10.6084\/m9.figshare.26491456.v5"},{"key":"e_1_3_2_37_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/978-3-031-47705-8_7","volume-title":"Proceedings of the 18th International Conference on integrated Formal Methods (iFM)","volume":"14300","author":"Paganoni Marco","year":"2023","unstructured":"Marco Paganoni and Carlo A. Furia. 2023. Reasoning about exceptional behavior at the level of Java bytecode. In Proceedings of the 18th International Conference on integrated Formal Methods (iFM), Paula Herber, Anton Wijs, and Marcello M. Bonsangue (Eds.). Lecture Notes in Computer Science, Vol. 14300, Springer, 113\u2013133."},{"key":"e_1_3_2_38_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/978-3-031-27481-7_20","volume-title":"Proceedings of the 25th International Symposium on Formal Methods (FM)","volume":"14000","author":"Paganoni Marco","year":"2023","unstructured":"Marco Paganoni and Carlo A. Furia. 2023. Verifying functional correctness properties at the level of Java bytecode. In Proceedings of the 25th International Symposium on Formal Methods (FM), Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker (Eds.). Lecture Notes in Computer Science, Vol. 14000, Springer, 343\u2013363."},{"key":"e_1_3_2_39_2","first-page":"201","volume-title":"Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2008, Seattle, WA, USA, July 20\u201324, 2008","author":"Papi Matthew M.","year":"2008","unstructured":"Matthew M. Papi, Mahmood Ali, Telmo Luis Correa Jr., Jeff H. Perkins, and Michael D. Ernst. 2008. Practical pluggable types for Java. In Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2008, Seattle, WA, USA, July 20\u201324, 2008, Barbara G. Ryder and Andreas Zeller (Eds.). ACM, 201\u2013212. DOI:DOI:10.1145\/1390630.1390656"},{"key":"e_1_3_2_40_2","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1145\/1328438.1328451","volume-title":"Proceedings of the POPL","author":"Parkinson Matthew J.","year":"2008","unstructured":"Matthew J. Parkinson and Gavin M. Bierman. 2008. Separation logic, abstraction and inheritance. In Proceedings of the POPL. 75\u201386."},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(3:1)2012"},{"key":"e_1_3_2_42_2","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/s00165-017-0435-1","article-title":"A fully verified container library","volume":"30","author":"Polikarpova Nadia","year":"2018","unstructured":"Nadia Polikarpova, Julian Tschannen, and Carlo A. Furia. 2018. A fully verified container library. Formal Aspects of Computing 30, 5 (2018), 495\u2013523.","journal-title":"Formal Aspects of Computing"},{"key":"e_1_3_2_43_2","first-page":"514","volume-title":"Proceedings of the 19th International Symposium on Formal Methods (FM) (Lecture Notes in Computer Science)","author":"Polikarpova Nadia","year":"2014","unstructured":"Nadia Polikarpova, Julian Tschannen, Carlo A. Furia, and Bertrand Meyer. 2014. Flexible invariants through semantic collaboration. In Proceedings of the 19th International Symposium on Formal Methods (FM) (Lecture Notes in Computer Science). Springer, 514\u2013530."},{"key":"e_1_3_2_44_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1007\/978-3-319-08867-9_7","volume-title":"Proceedings of the 26th International Conference on Computer Aided Verification, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18\u201322, 2014","volume":"8559","author":"Rakamaric Zvonimir","year":"2014","unstructured":"Zvonimir Rakamaric and Michael Emmi. 2014. SMACK: Decoupling source language details from verifier implementations. In Proceedings of the 26th International Conference on Computer Aided Verification, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18\u201322, 2014, Armin Biere and Roderick Bloem (Eds.). Lecture Notes in Computer Science, Vol. 8559, Springer, 106\u2013113. DOI:DOI:10.1007\/978-3-319-08867-9_7"},{"key":"e_1_3_2_45_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/978-3-540-68237-0_7","volume-title":"Proceedings of the 15th International Symposium on Formal Methods, FM 2008, Turku, Finland, May 26\u201330, 2008","volume":"5014","author":"Rudich Arsenii","year":"2008","unstructured":"Arsenii Rudich, \u00c1d\u00e1m Darvas, and Peter M\u00fcller. 2008. Checking well-formedness of pure-method specifications. In Proceedings of the 15th International Symposium on Formal Methods, FM 2008, Turku, Finland, May 26\u201330, 2008, Jorge Cu\u00e9llar, T. S. E. Maibaum, and Kaisa Sere (Eds.). Lecture Notes in Computer Science, Vol. 5014, Springer, 68\u201383. DOI:DOI:10.1007\/978-3-540-68237-0_7"},{"key":"e_1_3_2_46_2","first-page":"1:1","volume-title":"Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs, FTfJP@ECOOP 2019, London, United Kingdom, July 15, 2019","author":"R\u00fcmmer Philipp","year":"2019","unstructured":"Philipp R\u00fcmmer. 2019. JayHorn: A Java model checker. In Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs, FTfJP@ECOOP 2019, London, United Kingdom, July 15, 2019, Toby Murray and Gidon Ernst (Eds.). ACM, 1:1. DOI:DOI:10.1145\/3340672.3341113"},{"key":"e_1_3_2_47_2","volume-title":"Proceedings of the IWACO","author":"Summers Alexander J.","year":"2009","unstructured":"Alexander J. Summers, Sophia Drossopoulou, and Peter M\u00fcller. 2009. The need for flexible object invariants. In Proceedings of the IWACO. ACM, Article 6, 9 pages."},{"key":"e_1_3_2_48_2","first-page":"13","volume-title":"Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research, November 8\u201311, 1999, Mississauga, Ontario, Canada","author":"Vall\u00e9e-Rai Raja","year":"1999","unstructured":"Raja Vall\u00e9e-Rai, Phong Co, Etienne Gagnon, Laurie J. Hendren, Patrick Lam, and Vijay Sundaresan. 1999. Soot \u2013 a Java bytecode optimization framework. In Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research, November 8\u201311, 1999, Mississauga, Ontario, Canada, Stephen A. MacKay and J. Howard Johnson (Eds.). IBM, 13. Retrieved from https:\/\/dl.acm.org\/citation.cfm?id=782008"},{"key":"e_1_3_2_49_2","first-page":"419","volume-title":"Proceedings of the 19th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2004, October 24\u201328, 2004, Vancouver, BC, Canada","author":"Weimer Westley","year":"2004","unstructured":"Westley Weimer and George C. Necula. 2004. 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 24\u201328, 2004, Vancouver, BC, Canada. ACM, 419\u2013431. DOI:DOI:10.1145\/1028976.1029011"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3712015","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T13:20:43Z","timestamp":1762262443000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3712015"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,4]]},"references-count":48,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,12,31]]}},"alternative-id":["10.1145\/3712015"],"URL":"https:\/\/doi.org\/10.1145\/3712015","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2025,11,4]]},"assertion":[{"value":"2024-08-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-12-16","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}