Publications

• Planning for Autonomous Spacecraft Systems

  • Experimental Evaluation of a Planning Language Suitable for Formal Verification, Radu Siminiceanu, Rick Butler, and César Muñoz, Proceedings of the 5th International Workshop on Model Checking and Artificial Intelligence, BibTex Reference, 2009.
  • A Small-Step Semantics of PLEXIL, Gilles Dowek, César Muñoz, and Corina Pasareanu, BibTex Reference, 2008.
  • The ANMLite Language and Logic for Specifying Planning Problems, Ricky Butler, Radu Siminiceanu, and César Muñoz, NASA/TM-2006-214518, BibTex Reference, 2007.
  • 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), Ricky Butler, César Muñoz, and Radu Siminiceanu, NASA/TM-2006-214518, BibTex Reference, 2007.
  • A Formal Analysis Framework for PLEXIL, Gilles Dowek, César Muñoz, and Corina Pasareanu, 3rd Workshop on Planning and Plan Execution for Real-World Systems, BibTex Reference, 2007.
  • An Abstract Plan Preparation Language, Ricky Butler and César Muñoz, NASA/TM-2006-214518, BibTex Reference, 2006.

• Air Traffic Management Systems

  • A Formal Framework for the Analysis of Algorithms That Recover From Loss of Separation, Ricky Butler and César Muñoz, NASA/TM-2008-215356, BibTex Reference, 2008.
  • Conflict Prevention and Separation Assurance Method in the Small Aircraft Transportation System, Maria Consiglio, Víctor Carreño, Daniel Williams, and César Muñoz, Journal of Aircraft, BibTex Reference, 2008.
  • Safety and Performance Analysis of the Non-Radar Oceanic/Remote Airspace In-Trail Procedure, Víctor Carreño and César Muñoz, NASA/TM-2007-214856, BibTex Reference, 2007.
  • Conflict Detection and Resolution for 1,2,..,N Aircraft, Gilles Dowek and César Muñoz, 7th AIAA Aviation Technology, Integration and Operations Conference, BibTex Reference, 2007.
  • Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm, André Galdino, César Muñoz, and Mauricio Ayala, 14th Workshop on Logic, Language, Information and Computation, BibTex Reference, 2007.
  • Formal Analysis of the Operational Concept for the Small Aircraft Transportation System, César Muñoz, Víctor Carreño and Gilles Dowek, Rigorous Engineering of Fault-Tolerant Systems, BibTex Reference, 2006.
  • Safety Verification of the Small Aircraft Transportation System Concept of Operations, Víctor Carreño and César Muñoz, 5th AIAA Aviation, Technology, Integration, and Operations Conference, BibTex Reference, 2005.
  • Hybrid Verification of an Air Traffic Operational Concept, César Muñoz and Gilles Dowek, IEEE ISoLA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation, BibTex Reference, 2005.
  • KB3D Reference Manual - Version 1.a, César Muñoz, Radu Siminiceanu, Víctor Carreño, and Gilles Dowek, NASA/TM-2005-213769, BibTex Reference, 2005.
  • Provably Safe Coordinated Strategy for Distributed Conflict Resolution, Gilles Dowek, César Muñoz, and Víctor Carreño, AIAA Guidance Navigation, and Control Conference and Exhibit 2005, BibTeX Reference, 2005.
  • Implicit Intent Information for Conflict Detection and Alerting, Víctor Carreño and César Muñoz, Proceedings of the 23rd Digital Avionics Systems Conference, DASC 2004, BibTeX Reference, 2004.
  • Conflict Detection and Alerting in a Self Controlled Terminal Area, Maria Consiglio, César Muñoz, and Victor Carreño, Proceedings of the 24th Congress of International Council of Aeronautical Sciences, ICAS 2004, BibTex Reference, 2004.
  • Modeling and Verification of an Air Traffic Concept of Operations, César Muñoz, Gilles Dowek, and Victor Carreño, Proceedings of the International Symposium on Software Testing and Analysis, ISTTA 2004, BibTex Reference, 2004.
  • Formal Verification of a Conflict Resolution and Recovery Algorithm, Jeffrey Maddalon, Ricky Butler, Alfons Geser, and César Muñoz, NASA/TP-2004-213015, BibTex Reference, 2004.
  • Abstract Model of the SATS Concept of Operations: Initial Results and Recommendations, Gilles Dowek, César Muñoz, and Victor Carreño, NASA/TM-2004-213006, BibTex Reference, 2004.
  • Formal Analysis of Air Traffic Management Systems: The case of Conflict Resolution and Recovery, Ricky Butler, Alfons Geser, Jeffrey Maddalon, and César Muñoz, Proceedings of the 2003 Winter Simulation Conference, WSC 2003, BibTex Reference, 2003.
  • Formal verification of conflict detection algorithms, César Muñoz, Ricky Butler, Víctor Carreño, and Gilles Dowek, Software Tools for Technology Transfer, BibTeX Reference, 2003. Extended version available as NASA/TM-2001-210864, BibTeX Reference, 2001.
  • A Geometric Approach to Strategic Conflict Detection and Resolution, Alfons Geser and César Muñoz, Proceedings of the 21st Digital Avionics Systems Conference, DASC 2002, BibTex Reference, 2002.
  • Air Traffic Conflict Resolution and Recovery, Alfons Geser, César Muñoz, Gilles Dowek, and Florent Kirchner, ICASE Report 2002-12, BibTex Reference, 2002.
  • Tactical Conflict Detection and Resolution in a 3-D Airspace, Gilles Dowek, Alfons Geser, and César Muñoz, 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.
  • Aircraft Trajectory Modeling and Alerting Algorithm Verification, Víctor Carreño and César Muñoz, Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2000, BibTeX Reference, 2000. Extended version available as ICASE Report 2000-16, BibTeX Reference, 2000.
  • Formal Analysis of Parallel Landing Scenarios, Víctor Carreño and César Muñoz, Proceedings of the 19th Digital Avionics Systems Conference, DASC 2000, BibTeX Reference 2000.

• Theorem Proving and Model Checking

  • Verified Real Number Calculations: A Library for Interval Arithmetic, Marc Daumas, David Lester, César Muñoz, IEEE Transactions on Computers, BibTeX Reference, 2009.
  • Batch Proving and Proof Scripting in PVS, César Muñoz, NASA/CR-2007-214546, BibTex Reference, 2007.
  • Predicate Abstraction of Programs With Non-linear Computation, Songtao Xia, Ben Di Vito, and César Muñoz, Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006, BibTeX Reference, 2006.
  • PVS#: Streamlined Tacticals for PVS, Florent Kirchner and César Muñoz, Electronic Notes in Theoretical Computer Science, BibTeX Reference, 2006.
  • Provably Faithful Evaluation of Polynomials, Sylvie Boldo and César Muñoz, Proceedings of the 21st Annual ACM Symposium on Applied Computing, BibTeX Reference, 2006.
  • A High-Level Formalization of Floating-Point Numbers in PVS, Sylvie Boldo and César Muñoz, NASA/CR-2006-214298, BibTeX Reference, 2006.
  • Toward Automated Test Generation for Engineering Applications, Songtao Xia, Ben Di Vito, and César Muñoz, Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering, ASE 2005, BibTeX Reference, 2005.
  • Real Number Calculations and Theorem Proving, César Muñoz and David Lester, Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2005, BibTeX Reference, 2005. A draft version is available here.
  • Guaranteed Proofs Using Interval Arithmetic, Marc Daumas, Guillaume Melquiond, and César Muñoz, Proceedings of the 17th IEEE Symposium on Computer Arithmetic ARITH-17, BibTeX Reference, 2005.
  • Developing User Strategies in PVS: A Tutorial, Myla Archer, Ben Di Vito, and César Muñoz, Proceedings of Design and Application of Strategies/Tactics in Higher Order Logics, STRATRA 2003, NASA/CP-2003-212448, BibTex Reference, 2003.
  • Rapid prototyping in PVS, César Muñoz, NASA/CR-2003-212418, BibTex Reference, 2003.
  • Real Automation in the Field, César Muñoz and Micaela Mayero, Interim ICASE Report No. 39, BibTex Reference, 2001.
  • Towards a customizable PVS, Gerald Lüttgen, César Muñoz, Ricky Butler, Ben Di Vito, and Paul Miner, ICASE Report 2000-4, BibTex Reference, 2000.
  • Type Theory and Its Applications to Computer Science, César Muñoz , Quarterly News Letter of the Institute for Computer Applications in Science and Engineering (ICASE), BibTex Reference, 1999.
  • Structural Embeddings: Mechanization with Method, César Muñoz and John Rushby, Proceedings of the World Congress on Formal Methods FM 99, BibTex Reference, 1999. Also available as ICASE Report 1999-26, BibTex Reference, 1999.
  • PBS: Support for the B-Method in PVS, César Muñoz, SRI Technical Report SRI-CSL-99-01, BibTex Reference, 1999.
  • A Formalization of the B-Method in Coq and PVS, Jean Paul Bodeveix, Mamoun Filali, and César Muñoz, 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.

• Explicit Substitutions

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

  • The 21th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008), Lecture Notes in Computer Science, Vol. 5170, 2008.
  • Proceedings of the 6th International Workshop on Strategies in Automated Deduction (STRATEGIES 2006), Electronic Notes in Theoretical Computer Science, Volume 174, Issue 11, 2007.
  • Proceedings of Design and Application of Strategies/Tactics in Higher Order Logics (STRATRA 2003), NASA Conference Proceedings, NASA/CP-2003-212448, 2003.
  • The 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), Lecture Notes in Computer Science, Vol. 2410, 2002.