Laura Titolo

Laura Titolo

Principal Research Scientist

Code Metal

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 Code Metal, I am applying formal verification techniques to ensure the correctness and reliability of LLM-based code transpilation for edge computing, rapid prototyping, and code modernization applications. 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.

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:

POPL 2026 (PC) GeCoIn 2025 (PC) VSTTE 2025 (PC) NFM 2025 (General Chair), LOPSTR 2025 (PC co-chair), CPP 2025 (PC), PADL 2025(PC) 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)

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

Interests

Formal Methods Static Analysis Verification Abstract Interpretation Computational Logic
Recent News

Keynote @ ITP 2026

I am a keynote speaker at ITP 2025 in Reykjavik.

ITP 2026

I am in the Program Committee of ITP 2026.

NFM 2026

I am in the Program Committee of NFM 2026.

See all
Featured Publications
Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0 featured image

Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0

Laura Titolo
•
Read more
A Provably Correct Floating-Point Implementation of Well Clear Avionics Concepts featured image

A Provably Correct Floating-Point Implementation of Well Clear Avionics Concepts

Nikson Bernardes Fernandes Ferreira
•
Read more
Automatic Generation of Guard-Stable Floating-Point Code featured image

Automatic Generation of Guard-Stable Floating-Point Code

Laura Titolo
•
Read more
Eliminating Unstable Tests in Floating-Point Programs featured image

Eliminating Unstable Tests in Floating-Point Programs

Laura Titolo
•
Read more
A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm featured image

A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm

Laura Titolo
•
Read more
See all publications
Recent Publications
Laura Titolo, Mariano M. Moscato, Marco A. Feliu, Paolo Masci, Cesar A. Muñoz (2024). Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0. FM 2024.
PDF DOI
Lauren White, Laura Titolo, J. Tanner Slagel, Cesar A. Muñoz (2024). A Temporal Differential Dynamic Logic Formal Embedding. CPP 2024.
PDF DOI
Nikson Bernardes Fernandes Ferreira, Mariano M. Moscato, Laura Titolo, Mauricio Ayala-Rincon (2023). A Provably Correct Floating-Point Implementation of Well Clear Avionics Concepts. FMCAD 2023.
PDF DOI
Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, Aaron Dutle: (2022). A Compositional Proof Framework for FRETish Requirements. CPP 2022.
PDF DOI
Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, Gregory Anderson, And François Bobot (2021). Formal analysis of the compact position reporting algorithm. FAC 2021.
PDF DOI
See all publications
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.

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.

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.

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.

FPRoCK

FPRoCK is a software library for checking satisfiability of a set of mixed real and floating-point constraints.

See all

Experience

  1. Principal Research Scientist

    Code Metal
    • Development and application of formal methods techniques to ensure the quality and reliability of LLM-based code transpilation pipelines.

  2. 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.

  3. 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).

  4. 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.

  5. Researcher

    Technical University of Valencia
    • Design of a denotational semantics framework for the verification of temporal concurrent constraint programs (tccp).

Education

  1. PhD Computer Science

    University of Udine, Italy

  2. Diploma, Scientific Class

    Scuola Superiore, University of Udine, Italy

  3. MSc in Computer Science

    University of Udine, Italy

  4. BSc in Computer Science

    University of Udine, Italy