Seminars

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.

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.