César Muñoz's Publications

• Unmanned Aircraft Systems
• Air Traffic Management Systems
• Formal Methods
• Plan Execution and Planning
• Explicit Substitutions (1996-2001)
• Editor

Unmanned Aircraft Systems

• 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.
• 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.
• 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.
• 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.
• 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.
• 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, 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, Proceedings of the 2018 Aviation, Technology, Integration, and Operations Conference, 2018. 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.
• 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.
• 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.
• 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.
• 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, 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.
• 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.
• Jason Upchurch, César Muñoz, Anthony Narkawicz, James Chamberlain, and María Consiglio, Analysis of Well-Clear Boundary Models for the Integration of UAS in the NAS, Technical Memorandum, NASA/TM-2014-218280, June 2014. BibTeX Reference.
• César Muñoz, Anthony Narkawicz, James Chamberlain, María Consiglio, and Jason Upchurch, A Family of Well-Clear Boundary Models for the Integration of UAS in the NAS, Proceedings of the 14th AIAA Aviation Technology, Integration, and Operations (ATIO) Conference, AIAA-2014-2412, Atlanta, Georgia, 2014. BibTeX Reference.

Air Traffic Management Systems

• 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.
• 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, Washington D.C., 2016. 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.
• Anthony Narkawicz, César Muñoz, and George Hagen, An Independent and Coordinated Criterion for Kinematic Aircraft Maneuvers, Proceedings of the 14th AIAA Aviation Technology, Integration, and Operations (ATIO) Conference, AIAA-2014-2859, Atlanta, Georgia, 2014. BibTeX Reference.
• Parasara Sridhar Duggirala, Le Wang, Sayan Mitra, Mahesh Viswanathan, and César Muñoz, Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing Protocol, Proceedings of the 19th International Symposium on Formal Methods (FM 2014), Lecture Notes in Computer Science, Vol. 8442, pp. 215-229, 2014. BibTeX Reference.
• Anthony Narkawicz, César Muñoz, Jason Upchurch, James Chamberlain, and María Consiglio, A Well-Clear Volume Based on Time to Entry Point, Technical Memorandum, NASA/TM-2014-218155, January 2014. BibTeX Reference.
• César Muñoz, Anthony Narkawicz, and James Chamberlain, A TCAS-II Resolution Advisory Algorithm, Proceedings of the AIAA Guidance, Navigation, and Control Conference (GNC), AIAA-2013-4622, Boston, Massachusetts, August 2013. BibTeX Reference.
• Anthony Narkawicz, César Muñoz, Heber Herencia-Zapana, and George Hagen, Formal Verification of Lateral and Temporal Safety Buffers for State-Based Conflict Detection, Proceedings of the Institution of Mechanical Engineers, Part G: Journal of Aerospace Engineering, Vol. 227, No. 9, pp. 1412-1424, September 2013. BibTeX Reference.
• Anthony Narkawicz and César Muñoz, Formal Verification of Conflict Detection Algorithms for Arbitrary Trajectories, Reliable Computing, Volume 17, pp. 209-237, December, 2012. BibTeX Reference.
• Ricky Butler, George Hagen, Jeffrey Maddalon, César Muñoz, and Anthony Narkawicz, The search for effective algorithms for recovery from loss of separation, Proceedings of the 31st Digital Avionics Systems Conference (DASC 2012), Williamsburg, Virginia, 2012. BibTeX Reference.
• Anthony Narkawicz, César Muñoz, and Jeffrey Maddalon, A Mathematical Analysis of Air Traffic Priority Rules, Proceedings of the 12th AIAA Aviation Technology, Integration, and Operations (ATIO) Conference, AIAA-2012-5544, Indianapolis, Indiana, 2012. BibTeX Reference.
• María Consiglio, James Chamberlain, César Muñoz, and Keith Hoffler, Concept of integration for UAS operations in the NAS, Proceedings of the 28th International Congress of the Aeronautical Sciences (ICAS 2012), 2012. BibTeX Reference.
• Anthony Narkawicz, César Muñoz, and Gilles Dowek, Provably Correct Conflict Prevention Bands Algorithms, Science of Computer Programming, Volume 77, Issues 10-11, pp. 1039-1057, September 2012. BibTeX Reference.
• Anthony Narkawicz and César Muñoz, State-based implicit coordination and applications, Technical Publication, NASA/TP-2011-217067, March 2011. BibTeX Reference.
• César Muñoz, Ricky Butler, Anthony Narkawicz, Jeffrey Maddalon, and George Hagen, A Criteria Standard for Conflict Resolution: A Vision for Guaranteeing the Safety of Self-Separation in NextGen, Technical Memorandum, NASA/TM-2010-216862, October 2010. BibTeX Reference.
• César Muñoz and Anthony Narkawicz, Time of Closest Approach in Three-Dimensional Airspace, Technical Memorandum, NASA/TM-2010-216857, October 2010. BibTeX Reference.
• Heber Herencia-Zapana, Jean-Baptiste Jeannin, and César Muñoz, Formal Verification of Safety Buffers for State-Based Conflict Detection and Resolution, Proceedings of the 27th International Congress of the Aeronautical Sciences (ICAS 2010), 2010. BibTeX Reference.
• Anthony Narkawicz, César Muñoz, and Gilles Dowek, Formal verification of air traffic prevention bands algorithms, Technical Memorandum, NASA/TM-2010-216706, June 2010. BibTeX Reference.
• Ricky Butler, George Hagen, Jeffrey Maddalon, César Muñoz, Anthony Narkawicz, and Gilles Dowek, How Formal Methods Impels Discovery: A Short History of an Air Traffic Management Project, Technical Memorandum, NASA/CP-2010-216215, April 2010. BibTeX Reference.
• Jeffrey Maddalon, Ricky Butler, César Muñoz, and Gilles Dowek, A Mathematical Analysis of Conflict Prevention Information, 9th AIAA Aviation Technology, Integration, and Operations Conference, September 2009. BibTeX Reference. An extended version available as A Mathematical Basis for the Safety Analysis of Conflict Prevention Algorithms, Technical Memorandum, NASA/TM-2009-215768, June 2009. BibTeX Reference.
• Ricky Butler and César Muñoz, Formally Verified Practical Algorithms For Recovery From Loss of Separation, Technical Memorandum, NASA/TM-2009-215726, June 2009. BibTeX Reference.
• Ricky Butler and César Muñoz, A Formal Framework for the Analysis of Algorithms That Recover From Loss of Separation, Technical Memorandum, NASA/TM-2008-215356, October 2008. BibTeX Reference.
• María Consiglio, Víctor Carreño, Daniel Williams, and César Muñoz, Conflict Prevention and Separation Assurance Method in the Small Aircraft Transportation System, Journal of Aircraft, Volume 45, Number 0021-8669, 2008. BibTeX Reference.
• Víctor Carreño and César Muñoz, Safety and Performance Analysis of the Non-Radar Oceanic/Remote Airspace In-Trail Procedure, NASA/TM-2007-214856, BibTex Reference, 2007.
• Gilles Dowek and César Muñoz, Conflict Detection and Resolution for 1,2,..,N Aircraft,7th AIAA Aviation Technology, Integration and Operations Conference, BibTex Reference, 2007.
• André Galdino, César Muñoz, and Mauricio Ayala, Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm, 14th Workshop on Logic, Language, Information and Computation, BibTex Reference, 2007.
• César Muñoz, Víctor Carreño and Gilles Dowek, Formal Analysis of the Operational Concept for the Small Aircraft Transportation System, Rigorous Engineering of Fault-Tolerant Systems, BibTex Reference, 2006.
• Víctor Carreño and César Muñoz, Safety Verification of the Small Aircraft Transportation System Concept of Operations, 5th AIAA Aviation, Technology, Integration, and Operations Conference, BibTex Reference, 2005.
• César Muñoz and Gilles Dowek, Hybrid Verification of an Air Traffic Operational Concept, IEEE ISoLA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation, BibTex Reference, 2005.
• César Muñoz, Radu Siminiceanu, Víctor Carreño, and Gilles Dowek, KB3D Reference Manual - Version 1.a, NASA/TM-2005-213769, BibTex Reference, 2005.
• Gilles Dowek, César Muñoz, and Víctor Carreño, Provably Safe Coordinated Strategy for Distributed Conflict Resolution, AIAA Guidance Navigation, and Control Conference and Exhibit 2005, BibTeX Reference, 2005.
• Víctor Carreño and César Muñoz, Implicit Intent Information for Conflict Detection and Alerting, Proceedings of the 23rd Digital Avionics Systems Conference, DASC 2004, BibTeX Reference, 2004.
• Maria Consiglio, César Muñoz, and Victor Carreño, Conflict Detection and Alerting in a Self Controlled Terminal Area, Proceedings of the 24th Congress of International Council of Aeronautical Sciences, ICAS 2004, BibTex Reference, 2004.
• César Muñoz, Gilles Dowek, and Victor Carreño, Modeling and Verification of an Air Traffic Concept of Operations, Proceedings of the International Symposium on Software Testing and Analysis, ISTTA 2004, BibTex Reference, 2004.
• Jeffrey Maddalon, Ricky Butler, Alfons Geser, and César Muñoz, Formal Verification of a Conflict Resolution and Recovery Algorithm, NASA/TP-2004-213015, BibTex Reference, 2004.
• Gilles Dowek, César Muñoz, and Victor Carreño, Abstract Model of the SATS Concept of Operations: Initial Results and Recommendations, NASA/TM-2004-213006, BibTex Reference, 2004.
• Ricky Butler, Alfons Geser, Jeffrey Maddalon, and César Muñoz, Formal Analysis of Air Traffic Management Systems: The case of Conflict Resolution and Recovery, Proceedings of the 2003 Winter Simulation Conference, WSC 2003, BibTex Reference, 2003.
• César Muñoz, Ricky Butler, Víctor Carreño, and Gilles Dowek, Formal verification of conflict detection algorithms, Software Tools for Technology Transfer, BibTeX Reference, 2003. Extended version available as NASA/TM-2001-210864, BibTeX Reference, 2001.
• Alfons Geser and César Muñoz, A Geometric Approach to Strategic Conflict Detection and Resolution, Proceedings of the 21st Digital Avionics Systems Conference, DASC 2002, BibTex Reference, 2002.
• Alfons Geser, César Muñoz, Gilles Dowek, and Florent Kirchner, Air Traffic Conflict Resolution and Recovery, ICASE Report 2002-12, BibTex Reference, 2002.
• Gilles Dowek, Alfons Geser, and César Muñoz, Tactical Conflict Detection and Resolution in a 3-D Airspace, Proceedings of the Fourth International Air Traffic Management R&D Seminar ATM 2001, BibTeX Reference, 2001. Extended version available as ICASE Report 2001-7, BibTeX Reference, 2001.
• Víctor Carreño and César Muñoz, Aircraft Trajectory Modeling and Alerting Algorithm Verification, Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2000, BibTeX Reference, 2000. Extended version available as NASA/CR-2000-210097, BibTeX Reference, 2000.
• Víctor Carreño and César Muñoz, Formal Analysis of Parallel Landing Scenarios, Proceedings of the 19th Digital Avionics Systems Conference, DASC 2000, 2000.BibTeX Reference

Formal Methods

• 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.
• 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. Preprint.
• 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.
• 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.
• 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. 26:1-26: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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• Laura Titolo, Marco Feliu, Mariano Moscato, and César Muñoz, An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs, Proceedings 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.
• Anthony Narkawicz, César Muñoz, and Aaron Dutle, The MINERVA Software Development Process, Automated Formal Methods, Menlo Park, California, 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.
• 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.
• 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.
• 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.
• 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.
• Aaron Dutle, César Muñoz, Anthony Narkawicz, and Ricky Butler, Software Validation via Model Animation, 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, 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.
• Camilo Rocha, José Meseguer, and César Muñoz, Rewriting Modulo SMT and Open System Analysis, Proceedings of the 10th International Workshop on Rewriting Techniques and Applications (WRLA2014), Lecture Notes in Computer Science, Vol. 8663, pp. 247-262, 2014. BibTeX Reference.
• Anthony Narkawicz and César Muñoz, A Formally-Verified Decision Procedure for Univariate Polynomial Computation Based on Sturm’s Theorem, Technical Memorandum, NASA/TM-2014-218548, November 2014. BibTeX Reference.
• Andrew Smith, Luis Crespo, César Muñoz, and Mark Lowenberg, Bifurcation Analysis Using Rigorous Branch and Bound Methods, IEEE Multi-Conference on Systems and Control (MSC 2014), October 2014. BibTeX Reference.
• William Denman and César Muñoz, Automated Real Proving in PVS via MetiTarski, Proceedings of the 19th International Symposium on Formal Methods (FM 2014), Lecture Notes in Computer Science, Vol. 8442, pp. 194-199, 2014. BibTeX Reference.
• Anthony Narkawicz and César Muñoz, A Formally Verified Generic Branching Algorithm for Global Optimization, Proceedings of the Fifth Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE 2013), Lecture Notes in Computer Science, Vol. 8164, pp. 326-343, 2014. BibTeX Reference.
• Camilo Rocha, José Meseguer, and César Muñoz, Rewriting Modulo SMT, Technical Memorandum, NASA/TM-2013-218033, August 2013. BibTeX Reference.
• Alwyn Goodloe, César Muñoz, Florent Kirchner, and Löic Correnson, Verification of Numerical Programs: From Real Numbers to Floating Point Numbers, Proceedings of 5th NASA Formal Methods Symposium (NFM 2013), Lecture Notes in Computer Science, Vol. 7871, pp. 441-446, May 2013. BibTeX Reference.
• César Muñoz and Anthony Narkawicz, Formalization of a Representation of Bernstein Polynomials and Applications to Global Optimization, Journal of Automated Reasoning, Volume 51, Issue 2, pp. 151-196, August 2013. BibTeX Reference.
• Alwyn Goodloe and César Muñoz, Compositional Verification of a Communication Protocol for a Remotely Operated Aircraft, Science of Computer Programming, Volume 78, Issue 7, pp. 813-827, 2013. BibTeX Reference. This paper is an extended version of the conference publication in Lecture Notes in Computer Science, Volume 5825, November 2009.
• Anthony Narkawicz, Jürgen Garloff, Andrew Smith, and César Muñoz, Bounding the Range of a Rational Function over a Box, Reliable Computing, Volume 17, pp. 34-39, December, 2012. BibTeX Reference.
• César Muñoz and Ramiro Demasi, Advanced Theorem Proving Techniques in PVS and Applications, Tools for Practical Software Verification - LASER 2011, International Summer School, Lecture Notes in Computer Science, Volume 7682, pp. 97-133, 2012. BibTeX Reference.
• Luis Crespo, César Muñoz, Anthony Narkawicz, Sean Kenny, and Daniel Giesy, Uncertainty Analysis via Failure Domain Characterization: Polynomial Requirement Functions, European Safety and Reliability Conference, September 2011. BibTeX Reference.
• Florent Kirchner and César Muñoz, The Proof Monad, Journal of Logic and Algebraic Programming, Volume 79, Issues 3-5, pp. 264-277, April-July 2010. BibTeX Reference.
• Leonard Lensink, César Muñoz, and Alwyn Goodloe, From Verified Models to Verifiable Code, Technical Memorandum, NASA/TM-2009-215943, June 2009. BibTeX Reference.
• Alwyn Goodloe and César Muñoz, Design and Verification of a Distributed Communication Protocol, Lecture Notes in Computer Science, Volume 5825, November 2009. BibTeX Reference.
  A preliminary version appears as Contractor Report, NASA/CP-2009-215703, April 2009. BibTeX Reference.
• Marc Daumas, David Lester, and César Muñoz, Verified real number calculations: A library for interval arithmetic, IEEE Transactions on Computers, Volume 58, Number 2, 2009. BibTeX Reference.
• César Muñoz and Radu Siminiceanu, In-Trail Procedure (ITP) Algorithm Design, NASA Contractor Report,NASA/CR-2007-214863, August 2007. BibTeX Reference.
• César Muñoz, Batch Proving and Proof Scripting in PVS, NASA/CR-2007-214546, 2007. BibTex Reference.
• Songtao Xia, Ben Di Vito, and César Muñoz, Predicate Abstraction of Programs With Non-linear Computation, Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2006. BibTeX Reference.
• Florent Kirchner and César Muñoz, PVS#: Streamlined Tacticals for PVS, Electronic Notes in Theoretical Computer Science, Volume 174, Issue 11, July 2007. BibTeX Reference.
• Sylvie Boldo and César Muñoz, Provably Faithful Evaluation of Polynomials, Proceedings of the 21st Annual ACM Symposium on Applied Computing, 2006. BibTeX Reference.
• Sylvie Boldo and César Muñoz, A High-Level Formalization of Floating-Point Numbers in PVS, NASA/CR-2006-214298, 2006. BibTeX Reference.
• Songtao Xia, Ben Di Vito, and César Muñoz, Toward Automated Test Generation for Engineering Applications, Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2005. BibTeX Reference.
• César Muñoz and David Lester, Real Number Calculations and Theorem Proving, Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs), 2005. BibTeX Reference. A draft version is available here.
• Marc Daumas, Guillaume Melquiond, and César Muñoz, Guaranteed Proofs Using Interval Arithmetic, Proceedings of the 17th IEEE Symposium on Computer Arithmetic ARITH-17, 2005. BibTeX Reference.
• Myla Archer, Ben Di Vito, and César Muñoz, Developing User Strategies in PVS: A Tutorial, Proceedings of Design and Application of Strategies/Tactics in Higher Order Logics, STRATA 2003, NASA/CP-2003-212448, 2003. BibTex Reference.
• César Muñoz, Rapid prototyping in PVS, NASA/CR-2003-212418, 2003. BibTex Reference.
• César Muñoz and Micaela Mayero, Real Automation in the Field, NASA/CR-2001-211271, 2001. BibTex Reference.
• Gerald Lüttgen, César Muñoz, Ricky Butler, Ben Di Vito, and Paul Miner, Towards a customizable PVS, NACA/CR-2000-209851, 2000. BibTex Reference.
• César Muñoz, Type Theory and Its Applications to Computer Science, Quarterly News Letter of the Institute for Computer Applications in Science and Engineering (ICASE), 1999. BibTex Reference.
• César Muñoz and John Rushby, Structural Embeddings: Mechanization with Method, Proceedings of the World Congress on Formal Methods FM 99, 1999. BibTex Reference. Also available as ICASE Report 1999-26, 1999. BibTex Reference.
• César Muñoz, PBS: Support for the B-Method in PVS, SRI Technical Report SRI-CSL-99-01, BibTex Reference, 1999.
• Jean-Paul Bodeveix, Mamoun Filali, and César Muñoz, A Formalization of the B-Method in Coq and PVS, Electronic Proceedings of the B-User Group Meeting at the World Congress on Formal Methods FM 99, BibTex Reference, 1999. Version en français disponible.

Plan Execution and Planning

• Camilo Rocha and César Muñoz, Synchronous set relations in rewriting logic, Science of Computer Programming, Volume 92, Part B, pp. 211-228, 2014. BibTeX Reference.
• Camilo Rocha, Héctor Cadavid, César Muñoz, and Radu Siminiceanu, A Formal Interactive Verification Environment for the Plan Execution Interchange Language, Proceedings of 9th International Conference on Integrated Formal Methods (iFM 2012), Lecture Notes in Computer Science, Volume 7321, pp. 343-357, June 2012. BibTeX Reference.
• Camilo Rocha and César Muñoz, Simulation and Verification of Synchronous Set Relations in Rewriting Logic, Proceedings of 14th Brazilian Symposium on Formal Methods (SBMF 2011), Lecture Notes in Computer Science, Volume 7021, pp. 60-75, September 2011. BibTeX Reference.
• Camilo Rocha, César Muñoz, and Gilles Dowek, A Formal Library of Set Relations and Its Application to Synchronous Languages, Theoretical Computer Science, Volume 412, Issue 37, pp. 4853-4866, August 2011. BibTeX Reference.
• Gilles Dowek, César Muñoz, and Camilo Rocha, Rewriting Logic Semantics of a Plan Execution Language, Electronic Proceedings in Theoretical Computer Science, Volume 18, 2010. BibTeX Reference.
  A preliminary version appears as Technical Memorandum, NASA/TM-2009-215770, June 2009. BibTeX Reference.
• Radu Siminiceanu, Ricky Butler, and César Muñoz, Experimental Evaluation of a Planning Language Suitable for Formal Verification, 5th International Workshop on Model Checking and Artificial Intelligence (MoChArt 2008), Lecture Notes in Artificial Intelligence, Volume 5348, 2009. BibTeX Reference.
• Camilo Rocha, César Muñoz, and Héctor Cadavid, A Graphical Environment for the Semantic Validation of a Plan Execution Language, Third IEEE International Conference on Space Mission Challenges for Information Technology (SMC-IT 2009), 2009. BibTeX Reference.
• Erin Connors, César Muñoz, Cameron Schnur, and Radu Siminiceanu, Static Verification of Spacecraft Procedures, AIAA Infotech@Aerospace Conference 2009, AIAA 2009-2033, 2009. BibTeX Reference.
• Gilles Dowek, César Muñoz, and Corina Pasareanu, A Small-Step Semantics of PLEXIL, NIA Technical Report, Number 2008-11, 2008. BibTeX Reference.
• Ricky Butler, Radu Siminiceanu, and César Muñoz, The ANMLite Language and Logic for Specifying Planning Problems, NASA/TM-2007-215088, BibTex Reference, 2007.
• Ricky Butler, César Muñoz, and Radu Siminiceanu, Solving the AI Planning Plus Scheduling Problem Using Model Checking via Automatic Translation from the Abstract Plan Preparation Language (APPL) to the Symbolic Analysis Laboratory (SAL), NASA/TM-2007-215089, BibTex Reference, 2007.
• Gilles Dowek, César Muñoz, and Corina Pasareanu, A Formal Analysis Framework for PLEXIL, 3rd Workshop on Planning and Plan Execution for Real-World Systems, 2007. BibTeX Reference.
• Ricky Butler and César Muñoz, An Abstract Plan Preparation Language, NASA/TM-2006-214518, BibTex Reference, 2006.

Explicit Substitutions (1996-2001)

• César Muñoz, Proof-term synthesis on dependent-type systems via explicit substitutions, Theoretical Computer Science 266 (2001), BibTex Reference, 2001. Also available as ICASE Report 1999-47, BibTex Reference, 1999.
• César Muñoz, Dependent Types and Explicit Substitutions, Mathematical Structures in Computer Science 11 (2001), BibTex Reference, 2001. Also available as ICASE Report 1999-43, BibTex Reference, 1999.
• Mauricio Ayala-Rincón and César Muñoz, Explicit Substitutions and All That, Colombian Journal of Computer Science 1 (2000), BibTex Reference, 2000. Also available as ICASE Report 2000-45, BibTex Reference, 2000.
• Nikolaj Bjørner and César Muñoz, Absolute Explicit Unification, Proceedings of the 11th International Conference on Rewriting Techniques and Applications  RTA 2000, BibTex Reference, 2000.
• César Muñoz, Un calcul de substitutions pour la représentation de preuves partielles en théorie de types, Doctorate thesis, BibTex Reference, 1997. English version available as INRIA RR-3309, BibTex Reference, 1997.
• César Muñoz, A Left-Linear Variant of Lambda Sigma, Proceedings of the International Conference PLILP/ALP/HOA'97, BibTex Reference, 1997. Also available as INRIA RR-3107, BibTex Reference, 1997.
• César Muñoz, Proof Representation in Type Theory: From Incomplete Proofs to Incomplete Lambda-terms, Proceedings of the XXII Latin-American Conference of Informatics CLEI Panel 96, BibTex Reference, 1996.
• César Muñoz, Confluence and Preservation of Strong Normalisation in an Explicit Substitutions Calculus, Proceedings of the Eleven Annual IEEE Symposium on Logic in Computer Science LICS'96, BibTex Reference, 1996. Also available as INRIA RR-2762, BibTex Reference, 1996.

Editor

• 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.
• César Muñoz, Sanjai Rayadurgam, and Oksana Tkachuk, editors, Selected Extended Papers of NFM 2016, Special Issue, Journal of Automated Reasoning, Springer, 2017.
• 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, editor, Innovations in Systems and Software Engineering: Special Issue NFM 2010, Volume 7, Issue 2, 2011. BibTex Reference.
• César Muñoz, editor, Proceedings of the Second NASA Formal Methods Symposium (NFM2010), Conference Proceedings, NASA/CP-2010-216215, 2010. BibTex Reference.
• Hélène Kirchner and César Muñoz, editors, Proceedings of the First International Workshop on Strategies in Rewriting, Proving, and Programming (IWS2010), Electronic Proceedings of Theoretical Computer Science, Volume 44, 2010. BibTex Reference.
• Otmane Ait, César Muñoz, and Sofiène Tahar, editors, Proceedings of the 21st International Conference Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, Volume 5170, 2008. BibTex Reference.
• Myla Archer, Thierry Boy de la Tour, and César Muñoz, editors, Proceedings of the 6th International Workshop on Strategies in Automated Deduction (STRATEGIES 2006), Electronic Notes in Theoretical Computer Science, Volume 174, Issue 11, 2007.
• Myla Archer, Ben Di Vito, and César Muñoz, editors, Proceedings of Design and Application of Strategies/Tactics in Higher Order Logics (STRATRA 2003), NASA Conference Proceedings, NASA/CP-2003-212448, 2003.
• Víctor Carreño, César Muñoz, and Sofiène Tahar, editors, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), Lecture Notes in Computer Science, Vol. 2410, 2002.

The documents distributed by this server have been provided by the contributing authors as a mean to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the US Government, the authors, or by other copyright holders. The documents distributed by this server are the author's personal drafts of pre-prints of such papers and may not be reposted without the explicit permission of the copyright holder.

The tag identifies links that are outside the NASA domain