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), and Unmanned Aircraft Systems Integration in the National Airspace System (UAS in the NAS) projects. I am one of the main developers of ACCoRD (Airborne Coordinated Conflict Resolution and Detection), a framework for the formal analysis of state-based separation assurance systems, and of DAIDALUS (Detect and Aovid Alerting Logic for Unmanned Systems), a reference implementation of a detect and avoid concept for the integration of UAS into the national airspace system. Furthermore, I am permanent contributor to NASA's PVS Research effort.
- 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 (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
- The 11th International Workshop on Developments in Computational Models, 28 October 2015, Cali, Colombia. Post-workshop submission: December 7, 2015.
- 5th International ABZ Conference (ASM, Alloy, B, TLA, VDM, Z), May 23-27, 2016, Linz, Austria. Paper sumbission: January 15, 2016.
- 1st International Conference on Formal Structures for Computation and Deduction, June 22-26, 2016, Porto, Portugal. Abstract sumbission: January 29, 2016. Paper sumbission: February 5, 2016.
- 8th NASA Formal Methods Symposium, June 7-9, 2016, Minneapolis, MN. Abstract submission: February 19, 2016.