I am always looking for strong and motivated PhD students and postdocs to work with me on formal verification methods for data science and machine learning software. Contact me if interested!
I am a member of the INRIA research team ANTIQUE (ANalise 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 an invited speaker at Informatics 2024 in Poprad!
🎙 I am an invited speaker at FAC 2024 in Toulouse!
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.
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