NASA Langley Formal Methods • César Muñoz

César A. Muñoz

I earned an Engineering and a Master degree in Computer Science from the Universidad de los Andes (Bogotá), and a M.Sc. and Ph.D. in Computer Science from the University of Paris 7 (Paris). During my graduate studies, I was a Research Assistant in the Coq team at INRIA (Rocquencourt). After completing my Ph.D., I spent one and a half years as an International Fellow in the Computer Science Laboratory at SRI International (formerly, Stanford Research Institute) in Menlo Park. In 1999, I joined the Formal Methods group at ICASE - NASA Langley Research Center (LaRC). From 2003 to 2009, I worked for the National Institute of Aerospace. In 2009, I became a Research Computer Scientist at NASA, where I led the Formal Methods Team at NASA LaRC. This group supports the development of formal methods technologies for NASA's Airspace Operations and Safety Program (AOSP). From 2021 to 2023, I was a Sr. Principal Applied Scientist at Amazon (Amazon Web Services), where I managed the S3 Automated Reasoning Team. I rejoined NASA in 2023.

Projects

ACCoRD (Airborne Coordinated Conflict Resolution and Detection): Formal framework for the development of state-based separation assurance systems.
CPR (Compact Position Reporting): Formal analysis of the CPR algorithm, which is a safety-critical element of the Automatic Dependent Surveillance - Broadcast (ADS-B) protocol.
DAIDALUS (Detect and Avoid Alerting Logic for Unmanned Systems): Collection of formally verified detect and avoid algorithms for Unmanned Aircraft Systems.
DANTi (Detect and Avoid in the Cockpit): Assistive Detect and Avoid technology for manned aircraft.
DAA-Displays: A library of interactive graphical display elements (widgets) for cockpit systems, and simulations tools supporting comparative analysis of cockpit displays.
ICAROUS (Independent Configurable Architecture for Reliable Operations of Unmanned Systems): Software architecture that enables the robust integration of mission specific software modules and highly assured core software modules for building safety-centric autonomous unmanned aircraft applications.
Kodiak: Software library for the solution of numerical, possibly non-linear, problems over hyper-rectangular variable and parameter domains.
MINERVA (Mirrored Implementation Numerically Evaluated against Rigorously Verified Algorithms): Practical, but rigorous, approach to the development of safety-critical numerical software components.
Plaidypvs: Formal embedding of differential dynamic logic in the Prototype Verification System (PVS).
PLEXIL: Formal semantics and verification environment of NASA's Plan Execution Interchange Language (PLEXIL).
PolyCARP: Collection of formally verified algorithms and software for computations with polygons.
PRECiSA (Program Round-off Error Certifier via Static Analysis): Static analysis tool that generates provably correct round-off error bounds of floating-point functional expressions.
SIRUS (Simulation Infrastructure for Research on Interoperating Unmanned Systems): Research framework for simulation and analysis of future concepts for Urban Air Mobility (UAM) operations.
VSCode-PVS: Modern IDE for PVS based on Visual Studio Code.

Research

Theorem Proving: Research on theorem proving
UAS in the NAS: Detect and avoid concept for the integration of Unmanned Aircraft Systems in the National Airspace System
All publications
Older projects

In the News

"Testing shows drones can use autonomous technology to dodge other air traffic."
The Proof is On the Screen, Innovation Now, August 4, 2016.
NASA PVS Library featured in the movie “The Martian”.
NASA algorithms keep unmanned aircraft away from commercial aviation, NetworkWorld, July 14, 2015.
Formal Methods, Discovery Now, October 14, 2008.

Events

16th NASA Formal Methods Symposium (NFM 2024), Moffett Field, California, June 4-6, 2024.

Conferences and Journals

NASA Formal Methods Symposium (NFM)
Journal of Formalized Reasoning
Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, and Ivan Perez, editors, Selected Extended Papers of NFM 2021, Special Issue, Innovations in Systems and Software Engineering, Vol. 19, Issue 4, Springer, 2023.
Aaron Dutle, Mariano M. Moscato, Laura Titolo, César Muñoz, and Ivan Perez, editors, Proceedings of the 13th International Symposium, NFM 2021, Virtual Event, May 24–28, 2021, Lecture Notes in Computer Science, Volume 12673, Springer, 2021.
Aaron Dutle, César Muñoz, and Anthony Narkawicz, editors, Selected Extended Papers of NFM 2018, Special Issue, Innovations in Systems and Software Engineering, Vol. 15, Issues 3-4, Springer, 2019.
Mauricio Ayala-Rincón and César Muñoz, editors, Selected Extended Papers of ITP 2017, Special Issue, Journal of Automated Reasoning, Vol. 63, Issue 2, Springer, 2019.
Aaron Dutle, César Muñoz, and Anthony Narkawicz, editors, Proceedings of the 10th International Symposium, NFM 2018, Newport News, Virginia, USA, April 17–19, 2018, Lecture Notes in Computer Science, Volume 10811, Springer, 2018.
Mauricio Ayala-Rincón and César Muñoz, editors, Proceedings of the 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Lecture Notes in Computer Science, Volume 10499, Springer, 2017.
César Muñoz, Sanjai Rayadurgam, and Oksana Tkachuk, editors, Selected Extended Papers of NFM 2016, Special Issue, Journal of Automated Reasoning, Springer, 2017.

Recent Publications

2024

Lauren White, Laura Titolo, J. Tanner Slagel, and César Muñoz, A Temporal Differential Dynamic Logic Formal Embedding, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024), London, UK, 2024 [*]

+ Contact NASA