{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T04:11:28Z","timestamp":1746072688724,"version":"3.40.4"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031908996","type":"print"},{"value":"9783031909009","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Subtyping in object-oriented languages is widely based on Liskov\u2019s substitution principle, which offers static correctness guarantees of type safety while abstracting implementation details. Unfortunately, the type systems of languages like Java cannot statically enforce full behavioral substitutability, and in fact there are numerous examples of libraries some of whose components are related by inheritance but not substitutable (for example, because they do not implement \u201coptional\u201d operations).<\/jats:p>\n          <jats:p>In this paper, we present a novel approach to precisely specify and reason about substitutability in JVM languages. A distinctive feature of our approach is that it targets JVM bytecode, as opposed to a program\u2019s source code, as it is based on the <jats:sc>ByteBack<\/jats:sc> deductive verifier. To support reasoning about substitutability, we extended <jats:sc>ByteBack<\/jats:sc> with ghost specifications, a (restricted) form of class invariants, and substitutability-preserving specification inheritance (precondition weakening and postcondition strengthening). Equipped with these features, <jats:sc>ByteBack<\/jats:sc> can now reason precisely about behavioral substitutability violations in a way that is applicable to realistic examples (such as with optional operations of Java\u2019s  interface). Our experiments also demonstrate that <jats:sc>ByteBack<\/jats:sc> can analyze substitutability in programs written in a combination of JVM languages, including multi-language code where Scala or Kotlin code interacts with Java libraries.<\/jats:p>","DOI":"10.1007\/978-3-031-90900-9_12","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:45:26Z","timestamp":1745988326000},"page":"236-256","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Reasoning about Substitutability at the Level of JVM 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":[[2025,5,1]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bruns, D., Bubel, R., Gladisch, C., Grebing, S., H\u00e4hnle, R., Hentschel, M., Herda, M., Klebanov, V., Mostowski, W., Scheben, C., Schmitt, P.H., Ulbrich, M.: The KeY platform for verification and analysis of Java programs. In: Giannakopoulou, D., Kroening, D. (eds.) Verified Software: Theories, Tools and Experiments - 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers. Lecture Notes in Computer Science, vol.\u00a08471, pp. 55\u201371. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-12154-3_4, https:\/\/doi.org\/10.1007\/978-3-319-12154-3_4","DOI":"10.1007\/978-3-319-12154-3_4 10.1007\/978-3-319-12154-3_4"},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification\u2014The KeY Book, Lecture Notes in Computer Science, vol. 10001. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6, http:\/\/dx.doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Barnett, M., Chang, B.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A Modular Reusable Verifier for Object-Oriented P rograms. In: de\u00a0Boer, F.S., Bonsangue, M.M., Graf, S., de\u00a0Roever, W.P. (eds.) Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures. Lecture Notes in Computer Science, vol.\u00a04111, pp. 364\u2013387. Springer (2005). https:\/\/doi.org\/10.1007\/11804192_17, https:\/\/doi.org\/10.1007\/11804192_17","DOI":"10.1007\/11804192_17 10.1007\/11804192_17"},{"key":"12_CR4","doi-asserted-by":"publisher","unstructured":"Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O\u2019Hearn, P.W., Papakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving Fast with Software Verification. In: Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods - 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings. Lecture Notes in Computer Science, vol.\u00a09058, pp. 3\u201311. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_1, https:\/\/doi.org\/10.1007\/978-3-319-17524-9_1","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Cohen, E., Moskal, M., Schulte, W., Tobies, S.: Local verification of global invariants in concurrent programs. In: Proceedings of CAV. pp. 480\u2013494. Lecture Notes in Computer Science, Springer (2010)","DOI":"10.1007\/978-3-642-14295-6_42"},{"key":"12_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, France, April 6, 2014. EPTCS, vol.\u00a0149, pp. 79\u201392 (2014). https:\/\/doi.org\/10.4204\/EPTCS.149.8, https:\/\/doi.org\/10.4204\/EPTCS.149.8","DOI":"10.4204\/EPTCS.149.8 10.4204\/EPTCS.149.8"},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Dietl, W., Dietzel, S., Ernst, M.D., Muslu, K., Schiller, T.W.: Building and using pluggable type-checkers. In: Taylor, R.N., Gall, H.C., Medvidovic, N. (eds.) Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, Waikiki, Honolulu , HI, USA, May 21-28, 2011. pp. 681\u2013690. ACM (2011). https:\/\/doi.org\/10.1145\/1985793.1985889, https:\/\/doi.org\/10.1145\/1985793.1985889","DOI":"10.1145\/1985793.1985889 10.1145\/1985793.1985889"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Dovland, J., Johnsen, E.B., Owe, O., Steffen, M.: Lazy behavioral subtyping. J. Log. Algebraic Methods Program. 79(7), 578\u2013607 (2010). https:\/\/doi.org\/10.1016\/J.JLAP.2010.07.008, https:\/\/doi.org\/10.1016\/j.jlap.2010.07.008","DOI":"10.1016\/J.JLAP.2010.07.008 10.1016\/j.jlap.2010.07.008"},{"key":"12_CR9","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J., Gondelman, L., Paskevich, A.: The spirit of ghost code. Formal Methods Syst. Des. 48(3), 152\u2013174 (2016). https:\/\/doi.org\/10.1007\/S10703-016-0243-X, https:\/\/doi.org\/10.1007\/s10703-016-0243-x","DOI":"10.1007\/S10703-016-0243-X"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.J.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1\u201316:58 (2012). https:\/\/doi.org\/10.1145\/2187671.2187678, https:\/\/doi.org\/10.1145\/2187671.2187678","DOI":"10.1145\/2187671.2187678"},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Karakaya, K., Schott, S., Klauke, J., Bodden, E., Schmidt, M., Luo, L., He, D.: SootUp: A redesign of the Soot static analysis framework. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14570, pp. 229\u2013247. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57246-3_13, https:\/\/doi.org\/10.1007\/978-3-031-57246-3_13","DOI":"10.1007\/978-3-031-57246-3_13"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Kassios, I.T.: Dynamic frames: Support for framing, dependencies and sharing without restrictions. In: Proceedings of FM. pp. 268\u2013283. Lecture Notes in Computer Science, Springer (2006)","DOI":"10.1007\/11813040_19"},{"key":"12_CR13","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) (Oct 2011), https:\/\/www.bodden.de\/pubs\/lblh11soot.pdf"},{"key":"12_CR14","unstructured":"Leavens, G.T., Schmitt, P.H., Yi, J.: The Java Modeling Language (JML) (NII shonan meeting 2013-3). NII Shonan Meet. Rep. 2013 (2013), https:\/\/shonan.nii.ac.jp\/seminars\/016\/"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., M\u00fcller, P.: Object invariants in dynamic contexts. In: Proceedings of ECOOP. pp. 491\u2013516. Lecture Notes in Computer Science, Springer (2004)","DOI":"10.1007\/978-3-540-24851-4_22"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Schulte, W.: Using history invariants to verify observers. In: Proceedings of ESOP. pp. 80\u201394. Lecture Notes in Computer Science, Springer (2007)","DOI":"10.1007\/978-3-540-71316-6_7"},{"key":"12_CR17","doi-asserted-by":"publisher","unstructured":"Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811\u20131841 (1994). https:\/\/doi.org\/10.1145\/197320.197383, https:\/\/doi.org\/10.1145\/197320.197383","DOI":"10.1145\/197320.197383"},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Maddox, J., Long, Y., Rajan, H.: Large-scale study of substitutability in the presence of effects. In: Leavens, G.T., Garcia, A., Pasareanu, C.S. (eds.) Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/SIGSOFT FSE 2018, Lake Buena Vista, FL, USA, November 04-09, 2018. pp. 528\u2013538. ACM (2018). https:\/\/doi.org\/10.1145\/3236024.3236075, https:\/\/doi.org\/10.1145\/3236024.3236075","DOI":"10.1145\/3236024.3236075"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Marcilio, D., Furia, C.A.: Lightweight precise automatic extraction of exception preconditions in Java methods. Empirical Software Engineering 29(1), \u00a030 (2024)","DOI":"10.1007\/s10664-023-10392-x"},{"key":"12_CR20","unstructured":"Meyer, B.: Object-oriented software construction. Prentice Hall, 2nd edn. (1997)"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Owe, O.: Reasoning about inheritance and unrestricted reuse in object-oriented concurrent systems. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) Integrated Formal Methods - 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09681, pp. 210\u2013225. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_14, https:\/\/doi.org\/10.1007\/978-3-319-33693-0_14","DOI":"10.1007\/978-3-319-33693-0_14"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Paganoni, M., Furia, C.A.: Reasoning about exceptional behavior at the level of Java bytecode. In: Herber, P., Wijs, A., Bonsangue, M.M. (eds.) Proceedings of the 18th International Conference on integrated Formal Methods (iFM). Lecture Notes in Computer Science, vol. 14300, pp. 113\u2013133. Springer (November 2023)","DOI":"10.1007\/978-3-031-47705-8_7"},{"key":"12_CR23","doi-asserted-by":"crossref","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). Lecture Notes in Computer Science, vol. 14000, pp. 343\u2013363. Springer (March 2023)","DOI":"10.1007\/978-3-031-27481-7_20"},{"key":"12_CR24","doi-asserted-by":"publisher","unstructured":"Paganoni, M., Furia, C.A.: ByteBack FASE 2025 replication package (Jan 2025). https:\/\/doi.org\/10.6084\/m9.figshare.28166951.v4, https:\/\/doi.org\/10.6084\/m9.figshare.28166951.v4","DOI":"10.6084\/m9.figshare.28166951.v4"},{"key":"12_CR25","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, WA, USA, July 20-24, 2008. pp. 201\u2013212. ACM (2008). https:\/\/doi.org\/10.1145\/1390630.1390656, https:\/\/doi.org\/10.1145\/1390630.1390656","DOI":"10.1145\/1390630.1390656"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Tschannen, J., Furia, C.A., Meyer, B.: Flexible invariants through semantic collaboration. In: Proceedings of FM. Lecture Notes in Computer Science, vol.\u00a08442, pp. 514\u2013530. Springer (2014)","DOI":"10.1007\/978-3-319-06410-9_35"},{"key":"12_CR27","doi-asserted-by":"publisher","unstructured":"Pradel, M., Gross, T.R.: Automatic testing of sequential and concurrent substitutability. In: Notkin, D., Cheng, B.H.C., Pohl, K. (eds.) 35th International Conference on Software Engineering, ICSE\u201913, San Francisco, CA, USA, May 18-26, 2013. pp. 282\u2013291. IEEE Computer Society (2013). https:\/\/doi.org\/10.1109\/ICSE.2013.6606574, https:\/\/doi.org\/10.1109\/ICSE.2013.6606574","DOI":"10.1109\/ICSE.2013.6606574"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Summers, A.J., Drossopoulou, S., M\u00fcller, P.: The need for flexible object invariants. In: Proceedings of IWACO. pp.\u00a01\u20139. ACM (2009)","DOI":"10.1145\/1562154.1562160"},{"key":"12_CR29","doi-asserted-by":"publisher","unstructured":"Tempero, E.D., Yang, H.Y., Noble, J.: What programmers do with inheritance in Java. In: Castagna, G. (ed.) ECOOP 2013 - Object-Oriented Programming - 27th European Conference, Montpellier, France, July 1-5, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a07920, pp. 577\u2013601. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39038-8_24, https:\/\/doi.org\/10.1007\/978-3-642-39038-8_24","DOI":"10.1007\/978-3-642-39038-8_24"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90900-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:45:33Z","timestamp":1745988333000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90900-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031908996","9783031909009"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90900-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/fase\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}