## 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. From 2003 to 2008, I worked for the National Institute of Aerospace at Langley Research Center, where I led the NIA Formal Methods group. Since 2009, I have been a Research Computer Scientist at NASA.

I currently work on the development of formal methods technologies for NASA's Next Generation of Air Traffic Systems (NextGen), Validation and Verification of Flight Critical Systems (VVFCS), Unmanned Aircraft Systems Integration in the National Airspace System (UAS in the NAS), and Safe Autonomous Systems Operations (SASO) projects. I am permanent contributor to NASA's Formal Methods Research.

- ACCoRD (Airborne Coordinated Conflict Resolution and Detection): A 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): A collection of formally verified detect and avoid algorithms for Unmanned Aircraft Systems.
- ICAROUS (Integrated Configurable Algorithms for Reliable Operations of Unmanned Systems): A 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: A 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): A practical, but rigorous, approach to the development of safety-critical numerical software components.
- PLEXIL: Formal semantics and verification environment of NASA's Plan Execution Interchange Language (PLEXIL).
- PolyCARP: A collection of formally verified algorithms and software for computations with polygons.
- PRECiSA (Program Round-off Error Certifier via Static Analysis): A static analysis tool that generates provably correct round-off error bounds of floating-point functional expressions.

### Projects

### Research

- Formal Methods: Research in formal methods and theorem proving.
- UAS in the NAS: Detect and avoid concept for the integration of Unmanned Aircraft Systems in the National Airspace System.
- Publications.
- Older Projects.

### In The News

- 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

- 6th International ABZ (ASM, Alloy, B, TLA, VDM, Z) Conference, June 5th-8th, 2018, Southampton, UK.
- Tenth NASA Formal Methods Symposium (NFM 2018), Newport News, VA, USA. April 17-19, 2018.

### Conferences and Journals

- NASA Formal Methods Symposium (NFM)
- Journal of Formalized Reasoning
- 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 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

- 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 Formal Reasoning (accepted), 2018. - 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 Mendoç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. - 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,
*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. -
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. - 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, 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. - 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 paper of track 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 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 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 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.