I am a Senior Research Scientist at AMA Inc. working in the Safety-Critical Avionics Systems Branch at NASA Langley Research Center. I received my Ph.D. in Computer Science from the University of Udine (Italy) in May 2014. My PhD thesis was in part carried out at the Technical University of Valencia (Spain). I earned a Bachelor’s and a Master’s degree in Computer Science from the University of Udine, both received with full marks and honors (summa cum laude).
My research interests include every aspect of formal methods. In particular, I work on developing new tools for the formal verification and analysis of safety-critical avionics applications. I am currently working on improving the reliability of airspace software involving finite-precision computations.
Events: FMICS 2023 (PC co-chair), SAS 2023 (PC), ARITH 2023 (PC), LOPSTR 2023 (PC)
Past Events: NFM 2023 (PC) SAS 2022 (PC), LOPSTR 2022 (PC), SOAP 2022 (PC co-chair), CAV 2022 (PC) VMCAI 2022 (PC), CPP 2022 (PC), SOAP 2021 (PC), FMAS 2021 (PC), ESEC/FSE 2021 (PC Demonstration track), DETECT 2021 (PC) NFM 2021 (PC co-chair), NSV 2020 (PC), NFM 2020 (PC), FMAS 2020 (PC), DETECT 2020 (PC), NSV 2019 (PC), TNC 2018 (PC), NSV 2018 (PC), NFM 2018 (PC)
PhD in Computer Science, 2014
University of Udine, Italy
Diploma, Scientific Class, 2011
Scuola Superiore, University of Udine, Italy
MSc in Computer Science, 2010
University of Udine, Italy
BSc in Computer Science, 2008
University of Udine, Italy
I am PC co-chair of the 28rd International Conference on Formal Methods for Industrial Critical Systems (FMICS 2023) together with Alessandro Cimatti.
PRECiSA is a static analyzer that estimates the accumulated round-off error of floating-point programs.
It automatically generates PVS proof certificates that guarantee the correctness of the error estimations with respect to the floating-point IEEE-754 standard. It is designed to support a compositional static analysis of the program and it support a large variety of operators and program constructs.
ReFlow extracts floating-point C code from a PVS real numbers specification. The code is annotated with ACSL pre- and post-conditions that bound the accumulated round-off error.
ReFlow can also instrument the C code to detect when the floating-point control flow diverges with respect to the ideal real numbers' one.
VSCode-PRECiSA is a toolkit that integrates the PRECiSA floating-point round-off error analyzer into Visual Studio Code. The toolkit provides an intuitive graphical user interface and offers different analysis views for experimenting and reasoning about how floating-point errors affect the computed result of a program.
Rigorous PVS formalization of the Fretish structured natural language. It includes a new denotational semantics and a proof of semantic equivalence between Fretish specifications and their temporal logic counterparts computed by Fret.