César Muñoz's Publications
 Swee Balachandran, Viren Bajaj, Marco Feliú, César Muñoz, and María
Consiglio, A LearningBased 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), ATM201950, 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 OnBoard 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), AIAA20174484, 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 lidarbased 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 Lidarbased Geofences NASA Report on UTM Reference Mission Flights at
Southern Company Flights November 2016,
Technical Memorandum, NASA/TM2017219673,
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 EndtoEnd Verification and Validation (E2V2) Simulation,
Technical Memorandum, NASA/TM201720780,
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 HumanintheLoop Controller and Pilot Acceptability Study: Collision Avoidance
, SelfSeparation, and Alerting Times (CASSAT),
Technical Memorandum, NASA/TM2016219181,
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, HumanInTheLoop 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 WellClear
Definitions, Air Traffic Control Quarterly, Vol 23(4)
pp. 275299, 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 WellClear
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 (CAS1) Experiment Description and Initial Observations,
Technical Memorandum, NASA/TM2015218763,
May 2015. BibTeX Reference.
 Jason Upchurch, César Muñoz, Anthony Narkawicz, James Chamberlain, and María Consiglio,
Analysis of WellClear Boundary Models for the Integration of UAS in the NAS,
Technical Memorandum, NASA/TM2014218280,
June 2014. BibTeX Reference.
 César Muñoz, Anthony Narkawicz,
James Chamberlain, María Consiglio, and Jason Upchurch,
A Family of WellClear Boundary Models for the Integration of UAS in the NAS,
Proceedings of the 14th AIAA Aviation Technology, Integration, and Operations (ATIO) Conference, AIAA20142412,
Atlanta, Georgia, 2014. 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), AIAA20174491, 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), AIAA20162756, 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, AIAA20150795,
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, AIAA20142859,
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. 215229, 2014. BibTeX Reference.
 Anthony Narkawicz, César Muñoz, Jason Upchurch,
James Chamberlain, and María Consiglio,
A
WellClear Volume Based on Time to Entry Point,
Technical Memorandum, NASA/TM2014218155,
January 2014. BibTeX Reference.
 César Muñoz, Anthony Narkawicz, and James Chamberlain, A TCASII
Resolution Advisory Algorithm, Proceedings of the AIAA
Guidance, Navigation, and Control Conference (GNC), AIAA20134622,
Boston, Massachusetts, August 2013. BibTeX Reference.
 Anthony Narkawicz, César Muñoz, Heber
HerenciaZapana, and George Hagen, Formal
Verification of Lateral and Temporal Safety Buffers for StateBased
Conflict Detection, Proceedings of the Institution of
Mechanical Engineers, Part G: Journal of Aerospace Engineering,
Vol. 227, No. 9, pp. 14121424, 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. 209237, 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, AIAA20125544,
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 1011, pp. 10391057, September 2012. BibTeX Reference.
 Anthony Narkawicz and César Muñoz,
Statebased implicit coordination and applications,
Technical Publication, NASA/TP2011217067,
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 SelfSeparation in
NextGen,
Technical Memorandum, NASA/TM2010216862,
October 2010. BibTeX Reference.
 César Muñoz and Anthony Narkawicz, Time of Closest Approach in ThreeDimensional Airspace,
Technical Memorandum, NASA/TM2010216857,
October 2010. BibTeX
Reference.
 Heber HerenciaZapana, JeanBaptiste Jeannin, and César Muñoz, Formal Verification of Safety Buffers for StateBased 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/TM2010216706,
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/CP2010216215,
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/TM2009215768,
June 2009. BibTeX Reference.
 Jeffrey Maddalon, Ricky Butler, César Muñoz, and Gilles Dowek, A Mathematical Basis for the Safety Analysis of Conflict Prevention
Algorithms, Technical Memorandum, NASA/TM2009215768,
June 2009. BibTeX Reference.
 Ricky Butler and César Muñoz,
Formally Verified Practical Algorithms For Recovery From Loss of Separation,
Technical Memorandum, NASA/TM2009215726, 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/TM2008215356, 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 00218669, 2008.
BibTeX Reference.
 Víctor Carreño and César Muñoz, Safety and Performance Analysis of the NonRadar Oceanic/Remote Airspace InTrail Procedure,
NASA/TM2007214856, 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 FaultTolerant 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/TM2005213769, 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/TP2004213015, 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/TM2004213006, 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/TM2001210864, 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 200212, BibTex Reference, 2002.
 Gilles Dowek, Alfons Geser, and César Muñoz,
Tactical
Conflict Detection and Resolution in a 3D Airspace,
Proceedings of
the Fourth International Air Traffic Management R&D
Seminar ATM 2001, BibTeX
Reference, 2001. Extended version available as ICASE Report 20017,
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/CR2000210097, 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
 Mariano Moscato, Laura Titolo, Marco Feliú, and César
Muñoz, Provably Correct
FloatingPoint
Implementation of a PointinPolygon Algorithm, Proceedings
of the 3rd World Congress on Formal Methods (FM 2019), Lecture
Notes in Computer Science, Vol. 11800, pp. 2137, 2019. BibTeX Reference.
 Rocco Salvia, Laura Titolo, Marco A. Feliú, Mariano
M. Moscato, César Muñoz, and Zvonimir Rakamarić, A Mixed Real and FloatingPoint Solver ,
Proceedings of the 11th NASA Formal Methods Symposium (NFM 2019),
Lecture Notes in Computer Science,
Vol. 11460, pp. 363370, 2019. BibTeX Reference.
 Laura Titolo, César Muñoz, Marco Feliú,
and Mariano Moscato, Eliminating Unstable Tests in FloatingPoint Programs,
Proceedings of the 28th International Symposium on Logicbased
Program Synthesis and Transformation (LOPSTR 2018),
Frankfurt am Main, Germany, 2018.
Lecture
Notes in Computer Science, Vol. 11408, pp. 169183, 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/TM2018220117,
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. 1941, 2018. BibTeX Reference.
 Thiago Mendoça Ferreira Ramos, César
Muñoz, Mauricio AyalaRincó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. 196209, 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. 477494, 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. 647652, 2018. BibTeX Reference.
 Laura Titolo, Mariano Moscato, César
Muñoz, Aaron
Dutle, and François Bobot, A Formally Verified
FloatingPoint 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. 364381, 2018. BibTeX Reference.
 Laura Titolo, Marco Feliu, Mariano Moscato, and César
Muñoz, An Abstract
Interpretation Framework for the RoundOff Error Analysis of
FloatingPoint Programs, Proceedings 19th International Conference on
Verification, Model Checking, and Abstract Interpretation (VMCAI
2018), Lecture Notes in Computer Science,
Vol. 10747, pp. 516537, 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. 1934, 2017. BibTeX Reference.
 Mariano Moscato, Laura Titolo, Aaron Dutle, and César
Muñoz, Automatic Estimation of
Verified FloatingPoint RoundOff 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. 213229, 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. 247262, 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. 6776, 2016. BibTeX Reference.
 César Muñoz and Anthony Narkawicz, Formal analysis of extended wellclear boundaries for unmanned aircraft,
Proceedings of the 8th NASA Formal Methods Symposium (NFM 2016),
Lecture Notes in Computer Science,
Vol. 9690, pp. 221226, 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. 5862, 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 RealNumber Proving,
Proceedings of the 6th International Conference on Interactive
Theorem Proving (ITP 2015), Lecture Notes in Computer Science, Vol. 9236, pp. 294309, 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/TM2015218776,
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. 92108, 2015. BibTeX Reference.
 Anthony Narkawicz, César Muñoz, and Aaron Dutle,
FormallyVerified Decision Procedures for Univariate Polynomial
Computation Based on Sturm’s and Tarski’s Theorems, Journal
of Automated Reasoning, Volume 54, Issue 4, pp. 285326, 2015. DOI: 10.1007/s108170159320x. 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. 247262, 2014. BibTeX Reference.
 Anthony Narkawicz and César Muñoz, A
FormallyVerified Decision Procedure for Univariate Polynomial
Computation Based on Sturm’s Theorem, Technical Memorandum, NASA/TM2014218548, November
2014. BibTeX Reference.
 Andrew Smith, Luis Crespo, César Muñoz, and Mark Lowenberg,
Bifurcation Analysis Using Rigorous Branch and Bound Methods,
IEEE MultiConference 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. 194199, 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. 326343, 2014. BibTeX Reference.
 Camilo Rocha, José Meseguer, and César Muñoz,
Rewriting Modulo SMT, Technical Memorandum, NASA/TM2013218033, 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. 441446, 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. 151196, 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. 813827, 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. 3439, 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. 97133, 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 35, pp. 264277, AprilJuly 2010. BibTeX Reference.
 Leonard Lensink, César Muñoz, and Alwyn Goodloe,
From Verified Models to Verifiable Code, Technical Memorandum, NASA/TM2009215943, 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/CP2009215703,
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, InTrail Procedure (ITP)
Algorithm Design, NASA Contractor Report,NASA/CR2007214863, August 2007. BibTeX
Reference.
 César Muñoz, Batch Proving and Proof Scripting in
PVS, NASA/CR2007214546,
2007. BibTex
Reference.
 Songtao Xia, Ben Di Vito, and César Muñoz,
Predicate
Abstraction of Programs With Nonlinear 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 HighLevel Formalization of FloatingPoint Numbers in PVS,
NASA/CR2006214298, 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
ARITH17, 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/CP2003212448, 2003.
BibTex Reference.
 César Muñoz,
Rapid prototyping in PVS,
NASA/CR2003212418,
2003. BibTex
Reference.
 César Muñoz and Micaela Mayero,
Real Automation in the Field,
NASA/CR2001211271, 2001.
BibTex Reference.
 Gerald Lüttgen, César Muñoz, Ricky Butler,
Ben Di Vito, and Paul Miner,
Towards a customizable PVS,
NACA/CR2000209851, 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 199926, 1999. BibTex
Reference.
 César Muñoz,
PBS: Support for the BMethod in PVS,
SRI Technical Report
SRICSL9901, BibTex Reference,
1999.
 JeanPaul Bodeveix, Mamoun Filali, and César Muñoz,
A
Formalization of the BMethod in Coq and PVS,
Electronic Proceedings
of the BUser Group Meeting at the World Congress on Formal Methods FM
99,
BibTex Reference,
1999. Version en français
disponible.
 Camilo Rocha and César Muñoz,
Synchronous
set relations in rewriting logic,
Science of Computer Programming, Volume 92, Part B, pp. 211228, 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. 343357, 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. 6075, 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. 48534866, 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/TM2009215770, 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 (SMCIT 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 20092033, 2009.
BibTeX Reference.
 Gilles Dowek, César Muñoz, and Corina Pasareanu, A
SmallStep
Semantics of PLEXIL, NIA Technical Report, Number 200811, 2008.
BibTeX Reference.
 Ricky Butler, Radu Siminiceanu, and César Muñoz,
The ANMLite Language and Logic for Specifying Planning Problems, NASA/TM2007215088, 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/TM2007215089, 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 RealWorld Systems, 2007.
BibTeX Reference.
 Ricky Butler and César Muñoz,
An Abstract Plan Preparation Language,
NASA/TM2006214518,
BibTex
Reference, 2006.
 César Muñoz, Proofterm
synthesis on dependenttype systems via explicit
substitutions,
Theoretical Computer Science 266 (2001),
BibTex
Reference, 2001. Also available as ICASE Report 199947, 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 199943, BibTex
Reference, 1999.
 Mauricio AyalaRincó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 200045, 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 RR3309,
BibTex
Reference, 1997.
 César Muñoz,
A LeftLinear Variant of Lambda Sigma,
Proceedings of the International
Conference PLILP/ALP/HOA'97,
BibTex
Reference, 1997. Also available as INRIA RR3107, BibTex
Reference, 1997.
 César Muñoz,
Proof Representation in Type Theory:
From Incomplete Proofs to Incomplete Lambdaterms,
Proceedings of the XXII LatinAmerican 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 RR2762,
BibTex Reference, 1996.
 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 AyalaRincón and César Muñoz,
editors, Selected
Extended Papers of ITP 2017, Special Issue, Journal of Automated
Reasoning, 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 AyalaRincó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/CP2010216215, 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/CP2003212448, 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 preprints 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