NASA logo

+ Contact NASA



  • + HOME
  • + WELCOME
  • + QUICK PAGE
  • + PHILOSOPHY
  • + TEAM
  • + RESEARCH
  • + LINKS

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

    Research

    In the News

    Events

    Conferences and Journals

    Recent Publications

    2024

  • 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. 12934, pp. 322-328[*]. 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

    The tag [*] identifies links that are outside the NASA domain

    Contact

    Safety Critical Avionics Systems Branch
    NASA Langley Research Center
    Mail Stop 234
    Hampton, VA 23681-2199, USA


    cesar.a.munoz@nasa.gov
    Phone: +1 (757) 864 1446
    Fax: +1 (757) 864 4234