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

• Certified Programs and Proofs 2025 (CPP 2025), Denver, Colorado, January 20-21, 2025. Abstract Deadline: September 10, 2024
• 17th NASA Formal Methods Symposium (NFM 2025), Hampton Roads, Virginia, US, Spring 2025.

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

James Chamberlain, Maria Consiglio, César Muñoz, and Paolo Masci, Assistive detect and avoid technology in urban air mobility environments, Proceedings of the 43rd Digital Avionics Systems Conference (DASC 2024), September-October 2024, San Diego, CA, USA. BibTeX Reference.

Paolo Masci, James Chamberlain, César Muñoz, and Maria Consiglio, DANTi: A tool for assistive detect and avoid research, Proceedings of the 43rd Digital Avionics Systems Conference (DASC 2024), September-October 2024, San Diego, CA, USA. BibTeX Reference.

J Tanner Slagel, Lauren M. White, Aaron Dutle, César Muñoz, and Nicolas Crespo, A verification framework for runtime assurance of autonomous UAS, Proceedings of the 43rd Digital Avionics Systems Conference (DASC 2024), September-October 2024, San Diego, CA, USA. BibTeX Reference.

Laura R. Humphrey and César A. Muñoz, Preliminary application of formal verification to an autonomy architecture for unmanned aircraft, Proceedings of the 34th International Congress of the Aeronautical Sciences (ICAS 2024), 2024. BibTeX Reference.

Laura Titolo, Mariano Moscato, Marco Feliu, Paolo Masci, and César Muñoz, Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0, Proceedings of the 26th International Symposium on Formal Methods (FM 2024), Lecture Notes in Computer Science, Vol. 14934, pp. 20-38. BibTeX Reference.

J Tanner Slagel, Lauren White, Aaron Dutle, César Muñoz, and Nicolas Crespo, A Formal Verification Framework for Runtime Assurance, Proceedings of the 16th NASA Formal Methods Symposium (NFM 2024), Lecture Notes in Computer Science, Vol. 14627, pp. 322-328. BibTeX Reference.

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. BibTeX Reference.

2023

César Muñoz, Mauricio Ayala-Rincón, Mariano Moscato, Aaron Dutle, Anthony Narkawicz, Ariane Alves Almeida, Andréia B. Avelar, and Thiago M. Ferreira, Formal Verification of Termination Criteria for First-Order Recursive Functions, Journal of Automated Reasoning, Volume 67, Number 4, 2023. BibTeX Reference. This paper is an extended version of the conference publication in Schloss Dagstuhl - Leibniz- Zentrum für Informatik, Article No. 26, pp. 1-17, 2021.

J Tanner Slagel, Mariano Moscato, Lauren White, César Muñoz, Swee Balachandran, and Aaron Dutle, Embedding Differential Dynamic Logic in PVS,Proceedings of the 18th International Workshop on Logical and Semantic Frameworks, with Applications, 2023. BibTeX Reference.

2022

J. Tanner Slagel, César Muñoz, Swee Balachandran, Mariano M. Moscato, Aaron Dutle, Paolo Masci, and Lauren White, Towards an implementation of differential dynamic logic in PVS, Proceedings of the 11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (SOAP 2022), 2022.. BibTeX Reference.

2021

Aaron Dutle, Mariano Moscato, Laura Titolo, César Muñoz, Gregory Anderson, and François Bobot, Formal Analysis of the Compact Position Reporting Algorithm, Formal Aspects of Computing, Volume 33, Number 1, pp. 65-86, 2021. BibTeX Reference. This paper is an extended version of the conference publication in Lecture Notes in Computer Science, Vol. 10951, pp. 364-381, 2018.

Andrew Peters, Brendan Duffy, Swee Balachandran, María Consiglio, and César Muñoz, SIRIUS: Simulation Infrastructure for Research on Interoperating Unmanned Systems, Proceedings of the 40th Digital Avionics Systems Conference (DASC 2021), Virtual Conference, US, 2021. BibTeX Reference.

César Muñoz, Mauricio Ayala-Rincón, Mariano Moscato, Aaron Dutle, Anthony Narkawicz, Ariane Alves Almeida, Andréia B. Avelar, and Thiago M. Ferreira, Formal Verification of Termination Criteria for First-Order Recursive Functions, Proceedings of the 12th International Conference on Interactive Theorem Proving (ITP 2021), Article No. 26, pp. 1-17, Schloss Dagstuhl - Leibniz- Zentrum für Informatik, 2021. BibTeX Reference

Katherine Cordwell, César Muñoz, and Aaron Dutle, Improving automated strategies for univariate quantifier elimination, Technical Memorandum, NASA/TM-20205010644, January 2021. BibTeX Reference.

2020

Laura Titolo, Mariano Moscato, Marco Feliú, and César Muñoz, Automatic Generation of Guard-Stable Floating-Point Code, Proceedings of the 16th International Conference on Integrated Formal Methods (iFM 2020), Lecture Notes in Computer Science, Vol. 12546, pp. 141–159, 2020. BibTeX Reference.

Aaron Dutle, César Muñoz, Esther Conrad, Alwyn Goodloe, Laura Titolo, Ivan Perez, Swee Balachandran, Dimitra Giannakopoulou, Anastasia Mavridou, and Thomas Pressburger, From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project, Proceedings of the Second Workshop on Formal Methods for Autonomous Systems (FMAS 2020), Electronic Proceedings in Theoretical Computer Science, Vol. 329, pp. 23–30, 2020. BibTeX Reference.

Andrew Peters, Swee Balachandran, Brendan Duffy, Kyle Smalling, María Consiglio, and César Muñoz, Flight Test Results of a Distributed Merging Algorithm for Autonomous UAS Operations, Proceedings of the 39th Digital Avionics Systems Conference (DASC 2020), Virtual Conference, US, 2020. BibTeX Reference.

Brendan Duffy, Swee Balachandran, Andrew Peters, Kyle Smalling, María Consiglio, Louis Glaab, Andrew Moore, and César Muñoz, Onboard Autonomous Sense and Avoid of Non-Conforming Unmanned Aerial Systems, Proceedings of the 39th Digital Avionics Systems Conference (DASC 2020), Virtual Conference, US, 2020. BibTeX Reference.

Sami Mian, Tyler Garrett, Alexander Glandon, Christopher Manderino, Swee Balachandran, César Muñoz, and Chester Dolph, Autonomous Spacecraft Inspection with Free-Flying Drones, Proceedings of the 39th Digital Avionics Systems Conference (DASC 2020), Virtual Conference, US, 2020. BibTeX Reference.

Swee Balachandran, Christopher Manderino, César Muñoz, and María Consiglio, A Decentralized Framework to Support UAS Merging and Spacing Operations in Urban Canyons, Proceedings of 2020 International Conference on Unmanned Aircraft Systems (ICUAS 2020), 2020. BibTeX Reference.

Brendon K. Colbert, J. Tanner Slagel, Luis G. Crespo, Swee Balachandran, and César Muñoz, PolySafe: A Formally Verified Algorithm for Conflict Detection on a Polynomial Airspace, Proceedings of 1st Virtual IFAC World Congress (IFAC-V 2020), 2020. BibTeX Reference.

Paolo Masci and César Muñoz, A Graphical Toolkit for the Validation of Requirements for Detect and Avoid Systems, Proceedings of the 14th International Conference on Tests and Proofs (TAP 2020), Lecture Notes in Computer Science, Vol. 12165, pp. 155-166, 2020. BibTeX Reference.

Brendan Duffy, Swee Balachandran, María Consiglio, Louis Glaab, César Muñoz, Kyle Smalling, Nicholas Rymer, David Bradley, David Hare, Richard Grube, Matthew Coldsnow, Scott Sims, Jeffrey Hill, and Mahyar Malekpour, Sense and Avoid Characterization of the ICAROUS Architecture , Technical Memorandum, NASA/TM-2020-220591, May 2020. BibTeX Reference.

2019

Paolo Masci and César Muñoz, An Integrated Development Environment for the Prototype Verification System, Electronic Proceedings in Theoretical Computer Science, Vol. 310, pp. 35-49, 2019. BibTeX Reference.

Mariano Moscato, Laura Titolo, Marco Feliú, and César Muñoz, Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm, Proceedings of the 3rd World Congress on Formal Methods (FM 2019), Lecture Notes in Computer Science, Vol. 11800, pp. 21-37, 2019. BibTeX Reference.

Swee Balachandran, Viren Bajaj, Marco Feliú, César Muñoz, and María Consiglio, A Learning-Based Guidance Selection Mechanism for a Formally Verified Sense and Avoid Algorithm, Proceedings of the 38th Digital Avionics Systems Conference (DASC 2019), San Diego, California, US, 2019. BibTeX Reference.

Víctor Carreño, María Consiglio, and César Muñoz, Analysis and Preliminary Results of a Concept for Detect and Avoid in the Cockpit, Proceedings of the 38th Digital Avionics Systems Conference (DASC 2019), San Diego, California, US, 2019. BibTeX Reference.

Rocco Salvia, Laura Titolo, Marco A. Feliú, Mariano M. Moscato, César Muñoz, and Zvonimir Rakamarić, A Mixed Real and Floating-Point Solver , Proceedings of the 11th NASA Formal Methods Symposium (NFM 2019), Lecture Notes in Computer Science, Vol. 11460, pp. 363-370, 2019. BibTeX Reference.

María Consiglio, Brendan Duffy, Swee Balachandran, Louis Glaab, and César Muñoz, Sense and Avoid Characterization of the Independent Configurable Architecture for Reliable Operations of Unmanned Systems, Proceedings of the 13th USA/Europe Air Traffic Management Research and Development Seminar (ATM2019), ATM-2019-50, 2019. BibTeX Reference.

2018

John Siratt, Luis Crespo, Anthony Narkawicz, and César Muñoz, The Number of Support Constraints for Overlapping Set Optimization with Nested Admissible Sets is Equal to One, Technical Memorandum, NASA/TM-2018-220117, October 2018. BibTeX Reference.

Laura Titolo, César Muñoz, Marco Feliú, and Mariano Moscato, Eliminating Unstable Tests in Floating-Point Programs, Proceedings of the 28th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2018), Frankfurt am Main, Germany, 2018. Lecture Notes in Computer Science, Vol. 11408, pp. 169-183, 2018. BibTeX Reference.

Swee Balachandran, Anthony Narkawicz, César Muñoz, and María Consiglio, A geofence violation prevention mechanism for small UAS, Proceedings of the 31st Congress of the International Council of the Aeronautical Sciences (ICAS 2018), Bello Horizonte, Brazil, 2018. BibTeX Reference.

Anthony Narkawicz, César Muñoz, and Aaron Dutle, Sensor Uncertainty Mitigation and Dynamic Well Clear Volumes in DAIDALUS (Best of Track Paper Award), Proceedings of the 37th Digital Avionics Systems Conference (DASC 2018), London, England, UK, 2018. BibTeX Reference.

Swee Balachandran, César Muñoz, María Consiglio, Marco Feliú and Anand Patel, Independent Configurable Architecture for Reliable Operation of Unmanned Systems with Distributed On-Board Services, Proceedings of the 37th Digital Avionics Systems Conference (DASC 2018), London, England, UK, 2018. BibTeX Reference.

Swee Balachandran, César Muñoz, and María Consiglio, Distributed Consensus to Enable Merging and Spacing of UAS in an Urban Environment, Proceedings of the 2018 International Conference on Unmanned Aircraft Systems (ICUAS 2018), Dallas, Texas, USA, 2018. BibTeX Reference.

Andrew J. Moore, Swee Balachandran, Steven Young, Evan Dill, Michael Logan, Louis Glaab, César A. Muñoz, and María Consiglio, Testing Enabling Technologies for Safe UAS Urban Operations (2018 Air Transportation Systems/Aircraft Operations Best Paper Award), Proceedings of the 2018 Aviation, Technology, Integration, and Operations Conference, 2018. BibTeX Reference.

Anthony Narkawicz, César Muñoz, and Aaron Dutle, A Decision Procedure for Univariate Polynomial Systems Based on Root Counting and Interval Subdivision, Journal of Formalized Reasoning, Vol. 11, Number 1, pp. 19-41, 2018. BibTeX Reference.

César Muñoz, Anthony Narkawicz, and Aaron Dutle, From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems, Proceedings of the 22nd International Symposium on Formal Methods (FM 2018) - Industry Day, Lecture Notes in Computer Science, Vol. 10951, pp. 647-652, 2018. BibTeX Reference.

Laura Titolo, Mariano Moscato, César Muñoz, Aaron Dutle, and François Bobot, A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm, Proceedings of the 22nd International Symposium on Formal Methods (FM 2018), Lecture Notes in Computer Science, Vol. 10951, pp. 364-381, 2018. BibTeX Reference.

Thiago Mendonça Ferreira Ramos, César Muñoz, Mauricio Ayala-Rincón, Mariano Moscato, Aaron Dutle, and Anthony Narkawicz, Formalization of the Undecidability of the Halting Problem for a Functional Language, Proceedings of the 25th Workshop on Logic, Language, Information, and Computation (WoLLIC 2018), Lecture Notes in Computer Science, Vol. 10944, pp. 196-209, 2018. BibTeX Reference.

Mariano Moscato, Carlos G. Lopez Pombo, César Muñoz, and Marco Feliú, Boosting the Reuse of Formal Specifications, Proceedings of the 9th International Conference on Interactive Theorem Proving (ITP 2018), Lecture Notes in Computer Science, Vol. 10895, pp. 477-494, 2018. BibTeX Reference.

Laura Titolo, Marco Feliú, Mariano Moscato, and César Muñoz, An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs, Proceedings of the 19th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2018), Lecture Notes in Computer Science, Vol. 10747, pp. 516-537, 2018. BibTeX Reference.

Andrew J. Moore, Matthew Schubert, Nicholas Rymer, Swee Balachandran, María Consiglio, César A. Muñoz, Joshua Smith, Dexter Lewis, Paul Schneider, Inspection of electrical transmission structures with UAV path conformance and lidar-based geofences, Proceedings of the 2018 IEEE Power & Energy Society Innovative Smart Grid Technologies Conference (ISGT), 2018. BibTeX Reference.

2017

Aaron Dutle, Mariano Moscato, Laura Titolo, and César Muñoz, A Formal Analysis of the Compact Position Reporting Algorithm , Proceedings of the 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017), Lecture Notes in Computer Science, Vol. 10712, pp. 19-34, 2017. BibTeX Reference.

Mariano Moscato, Laura Titolo, Aaron Dutle, and César Muñoz, Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis, Proceedings of the 36th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2017), Lecture Notes in Computer Science, Vol. 10488, pp. 213-229, 2017. BibTeX Reference.

Andrew J. Moore, Matthew Schubert, Nicholas Rymer, Swee Balachandran, María Consiglio, César A. Muñoz, Joshua Smith, Dexter Lewis, Paul Schneider, UAV Inspection of Electrical Transmission Infrastructure with Path Conformance Autonomy and Lidar-based Geofences NASA Report on UTM Reference Mission Flights at Southern Company Flights November 2016, Technical Memorandum, NASA/TM-2017-219673, October 2017. BibTeX Reference.

Anthony Narkawicz, César Muñoz, and Aaron Dutle, The MINERVA Software Development Process, Automated Formal Methods, Menlo Park, California, 2017. BibTeX Reference.

Swee Balachandran, Anthony Narkawicz, César Muñoz, and María Consiglio, A Path Planning Algorithm to Enable Well-Clear Low Altitude UAS Operation Beyond Visual Line of Sight, Proceedings of the 12th USA/Europe Air Traffic Management Research and Development Seminar (ATM2017), ATM-2017-16, 2017. BibTeX Reference.

Swee Balachandran, César Muñoz, and María Consiglio, Implicitly Coordinated Detect and Avoid Capability for Safe Autonomous Operation of Small UAS, Proceedings of the 17th AIAA Aviation Technology, Integration, and Operations Conference (ATIO 2017), AIAA-2017-4484, 2017. BibTeX Reference.

James Chamberlain, María Consiglio, and César Muñoz, DANTi: Detect and Avoid iN The Cockpit, Proceedings of the 17th AIAA Aviation Technology, Integration, and Operations Conference (ATIO 2017), AIAA-2017-4491, 2017. BibTeX Reference.

Rania W. Ghatas, Devin P. Jack, Dimitrios Tsakpinis and Michael J. Vincent, James L. Sturdy, César A. Muñoz, Keith D. Hoffler, Aaron M. Dutle, Robert Myer, Anna M. DeHaven and Tod Lewis, and Keith E. Arthur, Unmanned Aircraft Systems Minimum Operational Performance Standards End-to-End Verification and Validation (E2-V2) Simulation, Technical Memorandum, NASA/TM-2017-20780, January 2017. BibTeX Reference.

Camilo Rocha, José Meseguer, and César Muñoz, Rewriting Modulo SMT and Open System Analysis, Journal of Logical and Algebraic Methods in Programming, Volume 86, Issue 1, pp. 269–297, 2017.. BibTeX Reference. This paper is an extended version of the conference publication in Lecture Notes in Computer Science, Vol. 8663, pp. 247-262, 2014.

2016

María Consiglio, César Muñoz, George Hagen, Anthony Narkawicz, and Swee Balachandran, ICAROUS: Integrated Configurable Algorithms for Reliable Operations of Unmanned Systems, Proceedings of the 35th Digital Avionics Systems Conference (DASC 2016), Sacramento, California, USA, 2016. BibTeX Reference.

César Muñoz, Aaron Dutle, Anthony Narkawicz, and Jason Upchurch, Unmanned Aircraft Systems in the National Airspace System: A Formal Methods Perspective, ACM SIGLOG News, Vol. 3. Number 3, pp. 67-76, 2016. BibTeX Reference.

Anthony Narkawicz, César Muñoz, and Aaron Dutle, Coordination Logic for Repulsive Resolution Maneuvers, Proceedings of the 16th AIAA Aviation Technology, Integration, and Operations Conference (ATIO 2016), AIAA-2016-2756, 2016. BibTeX Reference.

César Muñoz and Anthony Narkawicz, Formal analysis of extended well-clear boundaries for unmanned aircraft, Proceedings of the 8th NASA Formal Methods Symposium (NFM 2016), Lecture Notes in Computer Science, Vol. 9690, pp. 221-226, 2016. BibTeX Reference.

James Comstock, Rania Ghatas, Michael Vincent, María Consiglio, César Muñoz , James Chamberlain, Paul Volk, and, Keith Arthur, Unmanned Aircraft Systems Human-in-the-Loop Controller and Pilot Acceptability Study: Collision Avoidance , Self-Separation, and Alerting Times (CASSAT), Technical Memorandum, NASA/TM-2016-219181, April 2016. BibTeX Reference.

2015

César Muñoz, Formal Methods in Air Traffic Management: The Case of Unmanned Aircraft Systems (Invited Lecture), Proceedings of the 12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015), Lecture Notes in Computer Science, Vol. 9399, pp. 58-62, 2015. BibTeX Reference.

Andrew Smith, César Muñoz, Anthony Narkawicz, and Mantas Markevicius, A Rigorous Generic Branch and Bound Solver for Nonlinear Problems, Proceedings of the 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, IEEE Computer Society Conference Publishing Services, 2015. BibTeX Reference.

Mariano Moscato, César Muñoz, and Andrew Smith, Affine Arithmetic and Applications to Real-Number Proving, Proceedings of the 6th International Conference on Interactive Theorem Proving (ITP 2015), Lecture Notes in Computer Science, Vol. 9236, pp. 294-309, 2015. BibTeX Reference.

César Muñoz, Anthony Narkawicz, George Hagen, Jason Upchurch, Aaron Dutle, María Consiglio, and James Chamberlain, DAIDALUS: Detect and Avoid Alerting Logic for Unmanned Systems, Proceedings of the 34th Digital Avionics Systems Conference (DASC 2015), Prague, Czech Republic, 2015. BibTeX Reference.

María Consiglio, César Muñoz, George Hagen, Anthony Narkawicz, Jason Upchurch, James Comstock, Rania Ghatas, Michael Vincent, and James Chamberlain, Human-In-The-Loop Experimental Research for Detect and Avoid, Proceedings of the 34th Digital Avionics Systems Conference (DASC 2015), Prague, Czech Republic, 2015. BibTeX Reference.

Andrew Smith, César Muñoz, Anthony Narkawicz, and Mantas Markevicius, Kodiak: An Implementation Framework for Branch and Bound Algorithms, Technical Memorandum, NASA/TM-2015-218776, July 2015. BibTeX Reference.

Jason Upchurch, César Muñoz, Anthony Narkawicz, María Consiglio, and James Chamberlain, Characterizing the Effects of a Vertical Time Threshold for a Class of Well-Clear Definitions, Air Traffic Control Quarterly, Vol 23(4) pp. 275-299, 2015. BibTeX Reference. Also appeared as Jason Upchurch, César Muñoz, Anthony Narkawicz, María Consiglio, and James Chamberlain, Characterizing the Effects of a Vertical Time Threshold for a Class of Well-Clear Definitions (Best of Track Paper Award), Proceedings of the 11th USA/Europe Air Traffic Management R&D Seminar, ATM 2015, Lisbon, Portugal, 2015. BibTeX Reference.

James Chamberlain, María Consiglio, James Comstock, Rania Ghatas, and César Muñoz, NASA Controller Acceptability Study 1 (CAS-1) Experiment Description and Initial Observations, Technical Memorandum, NASA/TM-2015-218763, May 2015. BibTeX Reference.

Anthony Narkawicz, César Muñoz, and Aaron Dutle, Formally-Verified Decision Procedures for Univariate Polynomial Computation Based on Sturm’s and Tarski’s Theorems, Journal of Automated Reasoning, Volume 54, Issue 4, pp. 285-326, 2015. DOI: 10.1007/s10817-015-9320-x. BibTeX Reference.

Aaron Dutle, César Muñoz, Anthony Narkawicz, and Ricky Butler, Software Validation via Model Animation, Proceedings of the Proceedings of the 9th International Conference on Tests and Proofs (TAP 2015), Lecture Notes in Computer Science, Vol. 9154, pp. 92-108, 2015. BibTeX Reference.

Anthony Narkawicz and César Muñoz, A Formally Verified Conflict Detection Algorithm for Polynomial Trajectories, Proceedings of the 2015 AIAA Infotech @ Aerospace Conference, AIAA-2015-0795, Kissimmee, Florida, 2015. BibTeX Reference.

Awards

• National Aeronautics and Space Administration Group Achievement Award to CPR (Compact Position Reporting) Verification Team, for outstanding contributions verifying the Compact Position Reporting Algorithm to support safety of Automatic Dependent Surveillance-Broadcast in National Airspace System, 2022.
• National Aeronautics and Space Administration Group Achievement Award to DAIDALUS Development Team, for outstanding contributions to the development of Detect and Avoid technology supporting the integration of Unmanned Aircraft Systems into the National Airspace System, 2019.
• National Aeronautics and Space Administration Group Achievement Award to UAS Detect and Avoid Team, for groundbreaking research that underpins a new national standard for detect-and-avoid systems that will enable UAS to be safely integrated into the National Airspace System, 2018.
• National Aeronautics and Space Administration Group Achievement Award to UAS Traffic Management (UTM) Team, for exemplary performance in demonstrating a low-altitude UAS aviation system by conducting first-of-their-kind field tests of a novel UAS Traffic Management platform, 2017.
• National Aeronautics and Space Administration Early Career Achievement Medal, for exceptional advancements to the field of Formal Methods and significant contributions to NASA's mission, 2016.
• National Aeronautics and Space Administration Group Achievement Award to Collision Avoidance, Self Separation, and Alerting Times (CASSAT) Team, for exceptional technical leadership and innovation in defining and executing the CASSAT experiment for UAS Integration in the NAS, 2016.
• National Aeronautics and Space Administration Group Achievement Award to Unmanned Aircraft System Self-Separation Sense-and-Avoid Interoperability Team, for exceptional technical leadership and innovation in developing minimum performance standards for UAS operations in the NAS, 2015.
• National Aeronautics and Space Administration Group Achievement Award to Advanced Air Transportation Technologies Team, for the highly successful research and technology transfer leading to improved operations of the National Aerospace System, 2005.
• National Aeronautics and Space Administration Award for Turning Goals into Reality, for valuable contributions to Small Aircraft Transportation Systems Project Team and exceptional progress toward the Increase Capacity and Mobility, 2005.

The tag identifies links that are outside the NASA domain