Reasoning about Substitutability at the Level of JVM Bytecode
Faculty of Informatics - Academic Studies Administration
Date: 3 April 2025 / 16:30 - 17:30
USI Campus EST, Room D0.02
Speaker: Marco Paganoni, Università della Svizzera italiana
Abstract: While Java’s subtyping requires subclasses to implement superclass methods, this only provides limited compliance with Liskov’s Substitution Principle (LSP). True behavioral subtyping instead requires subclasses to obey their superclasses’ behavioral contract, which is hard to express with traditional type systems. As an example, Java’s List interface requires the implementation of an add method, but the list returned by the List.of method is immutable, and will throw an UnsupportedOperationException at runtime. While this behavior is fully documented, it cannot be expressed using Java’s type system. In this presentation, I will showcase an extension to our ByteBack verification tool to support reasoning and verifying behavioral substitutability across multiple JVM languages.
Biography: Marco Paganoni is a PhD student under the supervision of Prof. Carlo Alberto Furia at the ATOM group. Prior to starting his PhD, Marco obtained his master’s degree in Software & Data Engineering at the Università della Svizzera italiana. His main research interest is the integration of formal software verification techniques.
Chair: Luca Chiodini
*************************
In February 2019, the Software Institute started its SI Seminar Series. Every Thursday afternoon, a researcher of the Institute will publicly give a short talk on a software engineering argument of their choice. Examples include, but are not limited to novel interesting papers, seminal papers, personal research overview, discussion of preliminary research ideas, tutorials, and small experiments.
On our YouTube playlist you can watch some of the past seminars. On the SI website you can find more details on the next seminar, the upcoming seminars, and an archive of the past speakers.