Senior Research Scientist

AMA Inc./NASA LaRC

Biography

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)

Interests
  • Formal Methods
  • Static Analysis and Verification
  • Abstract Interpretation
  • Formal Semantics of Programming Languages
  • Computational Logic
Education

  • 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

News

Jan 20, 2023
FMICS 2023

I am PC co-chair of the 28rd International Conference on Formal Methods for Industrial Critical Systems (FMICS 2023) together with Alessandro Cimatti.

Jan 19, 2023
NFM 2023

I am a member of the Program Commitee of the 15th NASA Formal Methods Symposium (NFM 2023).

Apr 16, 2022
NASA Group Achivement award for CPR

Aaron Dutle, Mariano Moscato, César A. Muñoz, and myself have received the NASA Group Achivement Award for our work on the formal analysis of the Compact Position Reporting Algorithm (CPR).
See all posts

Experience

 
 
 
 
 
Research Scientist
NASA LaRC
Sep 2015 – Present Hampton, VA, USA
Member of the NASA Langley Formal Methods Team (Safety Critical Avionics Systems Branch). Working under the AMA Inc. RSES contract.
 
 
 
 
 
Postdoctoral Researcher
University of Malaga
Sep 2014 – Sep 2015 Malaga, Spain
Member of the Mobile Systems and Software Reliability (MORSE) team.
 
 
 
 
 
PhD Student
University of Udine
Sep 2010 – Apr 2014 Udine, Italy
 
 
 
 
 
Researcher
Univestitat Politecnica de Valencia
Jan 2010 – Mar 2010 Valencia, Spain

Recent Publications

Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, Aaron Dutle (2022). A Compositional Proof Framework for FRETish Requirements. CPP 2022.

PDF Cite Project 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 Cite DOI

Aaron Dutle, César A. Muñoz, Esther Conrad, Alwyn Goodloe, Laura Titolo, Ivan Perez, Swee Balachandran, Dimitra Giannakopoulou, Anastasia Mavridou, and Thomas Pressburger (2020). From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project. FMAS 2020.

PDF Cite DOI

Laura Titolo, Mariano M. Moscato, Marco A. Feliu, and Cesar A. Muñoz (2020). Automatic Generation of Guard-Stable Floating-Point Code. iFM 2020.

PDF Cite Project DOI

Mariano M. Moscato, Laura Titolo, Marco A. Feliu, and Cesar A. Muñoz (2019). Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm. FM 2019.

PDF Cite DOI

See all publications

Software

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.

Code

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.

Code

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.

Code

CPR*

CPR* is a formally verified C implementation of the Compact Position Reporting (CPR) algorithm, a key component of the ADS-B standard responsible for encoding and decoding aircraft positions.

Code

FPRoCK

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

Code

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.

Code

Contact