I am a Computer Science PostDoc in the deepse group, at DEIB, Politecnico di Milano.
My research interests cover formal methods for the verification of safety-critical and real-time systems, focusing on temporal logic, formal languages and automata theory.
I am currently working on context-free temporal logic and model checking. In particular, I am developing new temporal logics based on Operator Precedence Languages, with the purpose of allowing better and more general modelling and specification of procedural programs.
I am involved in the PIACERE H2020 project, in which I am investigating ways of model checking Infrastructure-as-Code.
I am also interested in the verification of floating-point computations,
as well as approximate computing.
I am part of the fabulous TAFFO development team.
- 2022/01/28: I’ll be a member of the OOPSLA 2022 ERC + AEC
- 2021/11/05: I’ll be a member of the FIST 2022 PC
- 2021/10/25: I’ll be a member of the ECOOP 2022 ERC + AEC
- 2021/09/24: our paper “Verification of Programs with Exceptions through Operator-Precedence Automata” has been accepted at SEFM 2021!
- 2021/09/16: I’ll be a member of the ICST 2021 Poster Track PC
- 2021/06/23: I’ll be a member of the OOPSLA 2021 AEC
- 2021/04/19: our paper “Model-Checking Structured Context-Free Languages” has been accepted at CAV 2021!
- 2021/02/10: our ACM TOSEM paper “A Practical Approach to Verification of Floating-Point C/C++ Programs with math.h/cmath Functions” has been accepted for presentation in the Journal-First track of ICSE 2021!
Sometimes, you may also find me here:
DEIB – Politecnico di Milano
Office 001, Floor 3, Building 22
Via Camillo Golgi 42, 20133 Milan, Italy
+39 02 2399 3707