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 and one of the main developers of
- DAIDALUS (Detect and Avoid Alerting Logic for Unmanned Systems), a collection of formally verified detect and avoid algorithms for Unmanned Aircraft Systems,
- ACCoRD (Airborne Coordinated Conflict Resolution and Detection), a formal framework for the development of state-based separation assurance systems, and
- Kodiak, a software library for the solution of numerical, possibly non-linear, problems over hyper-rectangular variable and parameter domains.
- NASA PVS Library featured in the movie “The Martian”.
- 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.
- 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.
Conferences and Journals
- 5th International ABZ Conference (ASM, Alloy, B, TLA, VDM, Z), May 23-27, 2016, Linz, Austria.
- 8th NASA Formal Methods Symposium, June 7-9, 2016, Minneapolis, MN.
- 1st International Conference on Formal Structures for Computation and Deduction, June 22-26, 2016, Porto, Portugal.
- IEEE 11avo Congreso Colombiano de Computación, September 27-30, 2016, Popayán, Colombia.