About
Laura Titolo is a Principal Research Scientist at Code Metal, where she applies formal methods to enhance the reliability of code transpilation for edge computing applications. Previously, she served as a Lead Research Scientist at NASA Langley Research Center, contributing to the NASA Formal Methods team in the Safety-Critical Avionics Systems Branch. She holds a Ph.D. in Computer Science from the University of Udine, Italy, where she also earned her BSc and MSc with full honors.
- Ph.D. in Computer Science, University of Udine, Italy (2014)
- MSc in Computer Science, University of Udine, Italy (2010)
- BSc in Computer Science, University of Udine, Italy (2008)
Her research centers on formal methods, static analysis, abstract interpretation, and computational logic, with a focus on verifying floating-point programs and safety-critical systems. She has developed key tools such as PRECiSA for round-off error analysis and ReFlow for extracting verified floating-point C code from formal specifications. Her work ensures robustness in numerical computations essential for avionics and autonomous systems.
The 15 most recent publications reflect a strong trend in formal verification of numerical software, particularly floating-point arithmetic in safety-critical domains like avionics. Her work integrates abstract interpretation, theorem proving (PVS), and static analysis to detect and correct numerical instabilities, ensure control flow correctness, and generate formally verified code. Applications span air traffic algorithms, geofencing, and autonomous flight monitoring.
Scientific awards include:
- NASA Group Achievement Award (2021) for verifying the Compact Position Reporting Algorithm
Laura Titolo actively contributes to the academic community through program committee roles and leadership. She has served as Program Co-Chair for SOAP 2022, General Chair for NFM 2025, and PC member for numerous conferences including POPL, CPP, VMCAI, SAS, and PLDI. She mentors junior researchers and collaborates extensively with teams at NASA and academic institutions. Her current work at Code Metal extends formal methods to transpiled code in edge computing, ensuring correctness in distributed and resource-constrained environments.
She leads and contributes to several research projects:
- PRECiSA: Static analyzer for floating-point round-off errors with PVS proof certificates
- ReFlow: Tool for extracting floating-point C code from PVS real-number specifications
- VSCode-PRECiSA: Integration of PRECiSA into Visual Studio Code
- FRET Proof Framework: PVS formalization of FRETish requirements
- FPRoCK: Solver for mixed real and floating-point constraints
