📢 I have several open PhD positions:
Contact me if interested!
I am a member of the INRIA research team ANTIQUE (ANalyse StaTIQUE). Previously, I was a postdoctoral researcher at the Chair of Programming Methodology, led by Peter Müller at ETH Zurich. I completed my Ph.D. in Computer Science, working under the joint supervision of Radhia Cousot and Antoine Miné at École Normale Supérieure. I hold a Bachelor’s and a Master’s degree in Computer Science, both received with full marks and honors (summa cum laude) from the Università degli Studi di Udine.
My research interests span the whole spectrum of formal methods and aim at developing methods and tools to enhance the reliability of computer software and understanding complex software systems. My main area of expertise is static analysis based on abstract interpretation, which provides rigorous mathematical guarantees of the behavior of computer programs. I am currently engaged in a long-term research effort to enhance the understanding and reliability of data science software, which nowadays plays an increasingly important role in critical decision making in fields such as finance and medicine.
I am curating a personal (and unfinished) collection of (what I think is) good advice for academics.
🎙 I am an invited speaker at Informatics 2024 in Poprad!
PhD in Computer Science, 2015
École Normale Supérieure, Paris, France
MSc in Computer Science, 2011
Università degli Studi di Udine, Udine, Italy
BSc in Computer Science, 2009
Università degli Studi di Udine, Udine, Italy
The ForML project investigates the use of abstract interpretation and counterexample-guided abstraction refinement with the purpose of efficiently answering queries about semantic properties of machine learning models such as robustness, fairness, and explainability. We also aim to formally verify existing and novel algorithms for answering such queries, and to derive certified implementations.
The goal of SAIF is to use the vast knowledge accumulated over decades in formal methods to rethink them and address the novel safety concerns raised by machine learning-based systems. Through the synergy of a diverse consortium with complementary expertise, we aim to bring society closer to a state where it can benefit from achievements in machine learning without suffering undue consequences.
[…page under construction…]
The goal of the Libra project is to develop new analyses and tools to reason about and certify fairness of decision-making software.
The Lyra research project is a long-term research effort to enhance the understanding and reliabilty of data science software. It aims ad developing new practical and accessible analyses and tools to reason about and provide rigorous guarantees of the behavior of data analytics, big data, machine learning, and deep learning applications.
The goal of the FuncTion project was the development of a static analyzer which automatically infers ranking functions and sufficient precondition for program termination (and other liveness properties) by means of abstract interpretation.
Abstract Interpretation: Application to Verification and Static Analysis
M2, Master Parisien de Recherche en Informatique (MPRI), Université de Paris, France
Formal Methods for Machine Learning Pipelines Lipari Summer School on Abstract Interpretation 2024, Lipary, Italy.
Formal Methods for Machine Learning Pipelines Summer School on Role and effects of ARTificial Intelligence in Secure ApplicatioNs 2024 (ARTISAN 2024), Valence, France.
Formal Methods for Machine Learning Pipelines
16th Summer School on Verification Technology, Systems & Applications (VTSA 2024), Esch-sur-Alzette, Luxembourg.
Slides
Formal Methods for Machine Learning Pipelines
École Jeunes Chercheuses et Jeunes Chercheurs en Programmation 2024 (EJCP 2024), Argelès-sur-Mer, France.
Abstract Interpretation: Application to Verification and Static Analysis
M2, Master Parisien de Recherche en Informatique (MPRI), Université de Paris, France
Python Interface for the APRON Numerical Abstract Domain Library
Abstract Interpretation-based Static Analysis for (Conditional) Termination (and Other CTL Properties)
Perfectly Parallel Abstract Interpretation-based Fairness Certification for Neural Networks
Abstract Interpretation-based Static Analysis for Data Science Applications