ByteBack: Deductive Functional Verification of Bytecode programs

Software Institute

Date: 11 May 2023 / 16:30 - 17:30

USI Campus Est, room D0.03, Sector D // Online

Speaker: Marco Paganoni

Abstract:
Deductive software verification tools allow us to specify and prove functional (input/output) properties of programs. Functional properties are specified at the level of the source code of the program using constructs such as pre/postconditions of methods, and intermediate assertions. To target these properties, verification tools are required to analyze the source code, and model the semantics of the programming language. Modern programming languages evolve extremely fast, making it difficult for verification tools to support all their new features.  In this seminar I will present ByteBack, an automatic deductive verification tool targeting Java bytecode. Compared to source-level languages, intermediate representations offer a more stable set features. These can decouple the verification process of a program from the source language used to write it. An additional benefit of this decoupling is that it allows us to extend the verification approach to target multiple programming 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: Hassan Atwi

To join online please click here: https://tinyurl.com/22r2p4us 

Faculties