M.Moscato.
00 Ph.D. in Computer Science

Mariano
Moscato.

Formal methods for safety-critical systems.

Publications → Let's connect CV
Portrait of Mariano Moscato
10+ yrsformal verification research with NASA's LaRC Formal Methods Team
Key projectsled or co-led, such as NASALib, VSCode-PVS and PRECiSA
2014Ph.D., University of Buenos Aires
01 About

Safer systems, proved correct.

I earned my Ph.D. in Computer Science at the University of Buenos Aires in 2014, under the supervision of Marcelo Frías. I joined the National Institute of Aerospace as a postdoc shortly after, and since 2023 I have continued this work at Analytical Mechanics Associates.

I have always tried to facilitate and ease the construction and verification of safer systems by applying Formal Methods in the different stages of their life cycle. I am a key member of NASA Langley's Formal Methods Team, where I research formal verification of safety-critical systems.

In my current role I have also managed internship programs and fostered scientific collaborations with national and international partners.

Handcrafting syntactic truth since c. 2006. on interactive theorem proving
02 Active interests

What I work on.

02.1

Interactive Theorem Proving

Handcrafting syntactic truth since c. 2006. My poison of choice is the Prototype Verification System. I contribute to the prover and, more regularly, to its de-facto library: NASALib.

02.2

Formal Analysis of Programs

Lately, focused on the verification of floating-point programs, with particular emphasis on providing externally verifiable certificates about the correctness of the analysis.

02.3

Automating Interactive Provers

I've been part of a collaborative effort to implement several termination criteria in PVS, which also involved their actual formalization. I'm also working on an automatic counterexample generator for PVS based on SAT-solving.

03 Tools

Software I build.

03.1

PRECiSA

Program Round-off Error Certifier via Static Analysis. A fully automatic analyzer that estimates round-off errors of floating-point valued functional expressions, with externally verifiable certificates.

Visit page →
03.2

Dynamite

An extension of PVS that embeds a complete calculus for Alloy. It lets users improve the proof effort, for instance by analyzing new hypotheses with the aid of the Alloy Analyzer.

Visit page →
03.3

NASALib

The de-facto library of the Prototype Verification System, a project I co-lead and contribute to regularly.

04 Experience & education

Where I've worked.

  1. Jun 2023 – present

    Analytical Mechanics Associates, Inc.

    Research Scientist Associate Principal (Feb 2025–) · Research Scientist Lead (2024) · Research Scientist Sr. (2023)

    Formal verification of safety-critical systems as part of NASA Langley's Formal Methods Team.

  2. Jul 2014 – May 2023

    National Institute of Aerospace

    Research Scientist Sr. · Research Scientist II · Research Scientist I · Postdoctoral Scholar

    Research on formal verification techniques and their application to safety-critical systems.

  3. 2004 – 2014

    University of Buenos Aires

    Teaching Assistant · Head of Teacher Assistants · Computer Science Outreach Secretary

    Lectured and mentored students in BSc and MSc Computer Science courses. As Outreach Secretary (2012–2014), planned workshops, courses and symposiums to promote Computer Science, and obtained outreach grants to support them.

  4. B.S. 2003 · M.S. 2005 · Ph.D. 2014

    Education

    University of Buenos Aires, Argentina

    Ph.D. (2014), M.S. (2005) and B.S. (2003) in Computer Science.

05 Selected publications

Recent work.

  1. 2026
    Integration of Formal Methods in the Development of a Language for Autonomous Spacecraft Operations L. White, C. Muñoz, M. Feliú, M. Moscato, L. Humphrey · 45th Digital Avionics Systems Conference (DASC 2026), Orlando, FL
  2. 2025
    A PVS Library on the Infinitude of Primes B. B. de Oliveira Ribeiro, M. M. Moscato, T. A. de Lima, M. Ayala-Rincón · 18th Conference on Intelligent Computer Mathematics (CICM 2025), LNCS 16136, Springer
  3. 2025
    Verification of an Anti-Unification Algorithm in PVS M. Ayala-Rincón, T. A. de Lima, M. J. D. Lima, M. M. Moscato, T. Kutsia · 17th NASA Formal Methods Symposium (NFM 2025)
  4. 2024
    Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0 L. Titolo, M. Moscato, M. Feliu, P. Masci, C. Munoz · Formal Methods (FM 2024), LNCS 14934, Springer
  5. 2023
    A Provably Correct Floating-Point Implementation of Well Clear Avionics Concepts N. B. F. Ferreira, M. Moscato, L. Titolo, M. Ayala-Rincón · FMCAD 2023, TU Wien Academic Press
  6. 2023
    Formal Verification of Termination Criteria for First-Order Recursive Functions C. A. Muñoz, M. Ayala-Rincón, M. M. Moscato, A. Dutle, A. Narkawicz, et al. · Journal of Automated Reasoning, vol. 67, article 40
  7. 2023
    Floating-point round-off error analysis of safety-critical avionics software L. Titolo, M. Moscato, M. Feliu, A. Dutle, C. Munoz · Challenges of Software Verification, Springer
  8. 2020
    Formal Analysis of the Compact Position Reporting Algorithm A. Dutle, M. M. Moscato, L. Titolo, C. A. Muñoz, G. Anderson, F. Bobot · Formal Aspects of Computing, Springer
  9. 2018
    Boosting the Reuse of Formal Specifications M. M. Moscato, C. G. López Pombo, C. A. Muñoz, M. A. Feliú · ITP 2018, Oxford, LNCS 10895
  10. 2015
    Affine Arithmetic and Applications to Real-Number Proving M. M. Moscato, C. A. Muñoz, P. A. Smith · ITP 2015, LNCS 9236
  11. 2014
    Dynamite: A Tool for the Verification of Alloy Models Based on PVS M. M. Moscato, C. G. López Pombo, M. F. Frias · ACM Transactions on Software Engineering and Methodology, vol. 23, no. 2

Full list on dblp →

05.1 Awards & recognitions
  • 2025Best Paper Award runner-up at CICM 2025 (Conference on Intelligent Computer Mathematics), for "A PVS Library on the Infinitude of Primes". Shared with Bruno Berto de Oliveira Ribeiro, Thaynara Arielly de Lima and Mauricio Ayala-Rincón.
  • 2025Honorable Mention Award at NASA Formal Methods 2025, for "Verification of an Anti-Unification Algorithm in PVS". Shared with Mauricio Ayala-Rincón, Thaynara Arielly de Lima, Maria Júlia Dias Lima and Temur Kutsia.
  • 2024Internal AMA IRAD award for the project "Estimate Numerical Errors in Quantized Neural Networks" (ongoing).
  • 2022NASA Group Achievement Award, for outstanding contributions verifying the Compact Position Reporting Algorithm to support the safety of ADS-B in the National Airspace System. Shared with Aaron Dutle, César Muñoz and Laura Titolo.
  • 2018National Institute of Aerospace Best Paper Award, for "A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm".
  • 2007EASST Best Paper Award at ETAPS 2007, and TACAS'07 Student Coauthor Award (sponsored by Microsoft Research Cambridge).
05.2 Teaching & mentoring
  • NowCo-advisor, Ph.D. in Computer Science, University of Brasilia (student: Nikson Bernardes; with Mauricio Ayala). Expected 2027.
  • 2023Co-advisor of M.S. thesis "Improving the Safety of Automatically Generated Implementations", University of Brasilia.
  • 2021Co-advisor of M.S. thesis "Finite Model Finder for the PVS Interactive Theorem Prover", University of Buenos Aires. Tutorial "Program Validation and Verification in PVS" at CADE-28.
  • 2018"Validating Critical Systems with PVS", one-week course at the Summer School in Computer Science, Río Cuarto, Argentina.
  • 2017Tutorial "PVS for Computer Scientists" at ITP 2017, Brasília.