LOPSTR 2025
I am a program co-chair, together with Santiago Escobar, of the 35nd International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2025). Stay tuned for more details.
About Me
I am a Principal Research Scientist at Code Metal working on applying formal methods to improve the reliability of code transpilation techniques for edge computing applications. Previously, I was a Lead Research Scientist for the Safety-Critical Avionics Systems Branch at NASA Langley Research Center and member of the NASA Formal Methods team. 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 focuses on different aspects and applications of formal methods.
At NASA I was developing new tools for the formal verification and analysis of safety-critical avionics applications. In particular, I developed and applied rigorous techniques for improving the reliability of airspace software involving finite-precision computations.
I was the main developer of the PRECiSA round-off error static analyzer for floating-point programs and the ReFlow floating-point C code extractor.
In addition, I contributed to different PVS libraries for structured natural language requirements, hybrid systems’ verification, and temporal logics.
At Code Metal I am applying formal verification techniques to improve the quality of automatically transpiled code for edge computing.
I am an active member of the formal methods and programming languages communities, and I have served as program committee chair and member in several international conferences.
Upcoming events:
Past Events:
NSAD 2024 (PC), FMICS 2024 (PC), LOPSTR 2024 (PC), ARITH 2024 (PC), SAS 2023 (PC), ARITH 2023 (PC), LOPSTR 2023 (PC) 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)
Interests
- Formal Methods
- Static Analysis
- Verification
- Abstract Interpretation
- Computational Logic
Education
PhD 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
Featured Publications
Recent Publications
(2024).
Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0.
FM 2024.
(2024).
A Temporal Differential Dynamic Logic Formal Embedding.
CPP 2024.
(2023).
A Provably Correct Floating-Point Implementation of Well Clear Avionics Concepts.
FMCAD 2023.
(2022).
A Compositional Proof Framework for FRETish Requirements.
CPP 2022.
(2021).
Formal analysis of the compact position reporting algorithm.
FAC 2021.
Projects
PRECiSA
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.
Sep 9, 2024
ReFlow
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.
Sep 9, 2024
VSCode-PRECiSA
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.
Sep 9, 2024
FRET Proof Framework
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.
Jan 17, 2022
FPRoCK
FPRoCK is a software library for checking satisfiability of a set of mixed real and floating-point constraints.
May 7, 2019
Experience
Principal Research Scientist
Code Metal- Development and application of formal methods techniques to ensure the quality of transpiled code for edge computing applications.
Research Scientist
NASA LaRC- Member of the NASA Langley Formal Methods Team (Safety Critical Avionics Systems Branch).
- Development of new tools for the formal verification and analysis of safety-critical avionics applications.
- Main developer of the PRECiSA and ReFlow tools.
- Recepient of the 2021 NASA Group Achievement Award for outstanding contributions verifying the Compact Position Reporting Algorithm to support safety of Automatic Dependent Surveillance-Broadcast in the National Airspace System.
Postdoctoral Researcher
University of Malaga- Member of the Mobile Systems and Software Reliability (MORSE) team.
- Development of an abstract interpretation framework for the verification of hybrid concurrent constraint programs (hy-tccp).
PhD Student
University of Udine- Development of an abstract interpretation framework for the verification of temporal concurrent constraint programs (tccp).
- Research on abtract interpretation and semantics of progamming languages.
Researcher
Technical University of Valencia- Design of a denotational semantics framework for the verification of temporal concurrent constraint programs (tccp).
Education
PhD Computer Science
University of Udine, ItalyDiploma, Scientific Class
Scuola Superiore, University of Udine, ItalyMSc in Computer Science
University of Udine, ItalyBSc in Computer Science
University of Udine, Italy
Recent News
New position at Code Metal
I have accepted a new position as Principal Research Scientist at Code Metal.
NFM 2025
I am General Chair of the 17th NASA Formal Methods Symposium NFM 2025 that will be held at the University of William and Mary (Williamsburg, VA, USA) June 11-13, 2025. Submissions are due on December 13, 2025.