USI - Email

Archive / INF Seminars / INF_2023_05_11_Marco_Paganoni

USI - Email

	ByteBack: Deductive Functional Verification of Bytecode programs

Chair: Hassan Atwi

Thursday

11.05

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

16:30 - 17:30


	Marco Paganoni Università della Svizzera italiana

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.