César Muñoz (2007)

César Muñoz has been an invited professor in June 2007 funded by the UFR SEE of the University of Perpignan Via Domitia. He participated to the French-Algerian cycle of seminars. Report of his work is available from HAL.

From left to right : Jean Benkhelil (president of the UPVD), Marc Daumas (CNRS-LIRMM & ELIAUS), César Muñoz (invited professor) and Jean-Michel Horner (former president of the UPVD)

Professional Interest

My professional interest is in formal methods. Formal methods is the research area of computer science that aims the use of mathematical techniques to improve reliability and safety of software and hardware systems. I have worked on topics related to that area since my undergraduate and graduate studies at the University of the Andes, Bogotá. In those years, I focused my interest on rewriting techniques and formal specification via abstract data types [21].

As research assistant at INRIA, Rocquencourt, I extended my research interest to constructive logic, type theory, and higher-order logic. In my Master's thesis [22], I implemented a decision procedure for constructive logic in the proof assistant Coq. In my PhD thesis [23], I proposed a lambda-calculus of explicit substitutions for the representation of incomplete proof terms in the Calculus of Constructions [2, 4, 24, 25].

After my PhD, I was an international fellow at the Computer Science Laboratory SRI, Menlo Park. During my residence there, I got interested in the development of software verification tools. I developed an embedding of the B Method in SRI's Prototype Verification System (PVS) [5, 31] and a prototype of SRI's Symbolic Analysis Laboratory (SAL) [3].

Currently, I lead the Formal Methods group at the National Institute of Aerospace (NIA). At NIA, and before that at ICASE NASA Langley Research Center, I have applied formal techniques to the specification, analysis, and verification of digital systems of interest to NASA. During my tenure at NIA, I have been involved in the formal safety analysis of Air Traffic Management Systems. In particular, I have conducted research on the verification of air traffic conflict detection and resolution algorithms [612,14,15,17,18,20,27] and on the safety analysis of an advanced concept for air traffic operations [13, 28]. This effort has required fundamental research in the area of theorem proving that led to the development of several libraries, strategies, and tools [1, 16, 19, 26, 29, 30].

University Studies

  • Ph.D. in Computer Science, University of Paris 7, Paris. Subject: Representation and synthesis of proofs in Type Theory. Adviser: Gérard Huet.
  • Master's Thesis in Computer Science, University of Paris 7, Paris. Subject: Decision procedures for propositional intuitionistic logic. Adviser: Gilles Dowek.
  • Master's Thesis in Computer Science, University of the Andes, Bogotá. Subject: Verified implementation of Abstract Data Types. Adviser: Rodrigo Cardoso.
  • Engineering Degree in Computer Science, University of the Andes, Bogotá.

Research Experience

  • Senior staff scientist, National Institute of Aerospace, Langley Research Center, Hampton.
  • Staff scientist, ICASE - NASA Langley Research Center, Hampton.
  • International fellow, SRI International, Menlo Park.
  • Research assistant, INRIA, Rocquencourt.
  • Research assistant, University of the Andes, Bogotá.

Teaching Experience

  • Lecturer, NASA-NIA Formal Methods Training: PVS, NASA Langley Research Center and National Institute of Aerospace, Hampton.
  • Course on Formal Verification with PVS, University of La Coruna, La Coruna.
  • Lecturer, NASA-NIA Formal Methods Training: PVS, NASA Langley Research Center and National Institute of Aerospace, Hampton.
  • Master's course on Formal Verification of Software Systems, University of the Andes, Bogotá.
  • Lecturer, NASA Formal Methods Training: PVS, NASA Langley Research Center, Hampton.
  • Tutorial on Formal Methods, INT, Evry.
  • Master's course on Formal Methods, EAFIT University, Medell'in.
  • Teaching assistant, Master's course on Automated Deduction, University of the Andes, Bogotá.
  • Undergraduate course on Programming Languages, University of the Andes, Bogotá.
  • Teaching assistant, undergraduate course on Program Verification, University of the Andes, Bogotá.

Systems Tools

I have significantly contributed to the development of the following systems and tools.

Tool Description Prog. Lang.
Manta Abstract data type manager C
Tauto (Coq) Tactic for intuitionist propositional logic OCaml
Unofficial SAL First prototype of SAL Java
PBS (PVS) Embedding of the B Method Java
Field (PVS) Strategies for real number proving Lisp
PVSio (PVS) Ground evaluator extension Lisp
Besc (PVS) Explicit model checker Lisp
ProofLite (PVS) Proof checking in batch mode Lisp, Perl
Interval (PVS) Strategies for exact arithmetic Lisp

External Activities

  • Program Committee member of TPHOLs 2004.
  • Organizer and Program Committee member of the First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics, STRATA 2003.
  • Program Committee member of TPHOLs 2003.
  • Program Co-chair and Organizing Committee member of TPHOLs 2002, the International Conference on Theorem Proving in Higher Order Logics 2002.
  • Principal Investigator of a NSF Grant on the amount of $10.000 to support student participation at TPHOLs 2002.
  • Program Committee member of WESTAPP 2001, the Workshop on Explicit Substitutions and Applications 2001.
  • Program Committee member of LFM2000, the NASA Langley Formal Methods Workshop 2000.
  • Referee of several conferences and journals on formal methods, including Logics in Computer Science (LICS), Theorem Proving in Higher Order Logics (TPHOLs), Rewriting Techniques and Applications (RTA), Formal Methods Conference (FM), Workshop on Types (TYPES), Spin Workshop (SPIN), Langley Formal Methods (LFM), Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE), Protocol Specification, Testing and Verification (PSTV), Mathematical Structures in Computer Science (MSCS).

Publications

  • [1] M. Archer, B. Di Vito, and C. Munoz. Developing user strategies in PVS: A tutorial. In Proceedings of Design and Application of Strategies/Tactics in Higher Order Logics STRATA'03, NASA/TP-2003- 212448, NASA LaRC,Hampton VA 23681-2199, USA, September 2003.
  • [2] M. Ayala-Rinc'on and C. Munoz. Explicit substitutions and all that. Colombian Journal of Computer Science, 1(1):4771, December 2000. An earlier version appears as report NASA/CR-2000-210621 ICASE No. 2000-45.
  • [3] S. Bensalem, V. Ganesh, Y. Lakhnech, C. Munoz, S. Owre, H. Rueß, J. Rushby, V. Rusu, H. Saïdi, N. Shankar, E. Singerman, and A. Tiwari. An overview of SAL. Fifth NASA Langley Formal Methods Workshop LFM'2000, June 2000.
  • [4] N. Bjørner and C. Munoz. Absolute explicit unification. In International Conference on Rewriting Techniques and Applications (RTA'2000), volume 1833 of Lecture Notes in Computer Science, pages 3146, Norwich, U.K., July 2000.
  • [5] J.-P. Bodeveix, M. Filali, and C. Munoz. Formalisation de la méthode B en Coq et PVS. Technique et science informatique, 20(7):901926, 2001.
  • [6] R. Butler, A. Geser, J. Maddalon, and C. Munoz. Formal analysis of air traffic management systems: The case of conflict resolution and recovery. In Proceedings of the Winter Simulation Conference WSC'03, pages 906914, New Orleans, LA, December 2003. A long vesion appears as report NASA/TP-2004- 213015.
  • [7] R.W. Butler, V. Carreno, G. Dowek, and C. Munoz. Formal verification of conflict detection algorithms. In Proceedings of the 11th Working Conference on Correct Hardware Design and Verification Methods CHARME 2001, volume 2144 of LNCS, pages 403417, Livingston, Scotland, UK, 2001. A long version appears as report NASA/TM-2001-210864.
  • [8] V. Carreno and C. Munoz. Aircraft trajectory modeling and alerting algorithm verification. In J. Harrison and M. Aagaard, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science, pages 90105. Springer-Verlag, 2000. An earlier version appears as report NASA/CR-2000-210097 ICASE No. 2000-16.
  • [9] V. Carreno and C. Munoz. Formal analysis of parallel landing scenarios. In Proceedings of the 19th Digital Avionics Systems Conference, Philadelphia, PA, 2000.
  • [10] V. Carreno and C. Munoz. Implicit intent information for conflict detection and alerting. In Proceedings of the 23rd Digital Avionics Systems Conference, Salt Lake City, Utah, 2004.
  • [11] M. Consiglio, C. Munoz, and V. Carreno. Conflict detection and alerting in a self controlled terminal area. In Proceedings of 24th International Congress of the Aeronautical Sciences, ICAS 2004, Yokohama, Japan, 2004.
  • [12] G. Dowek, A. Geser, and C. Munoz. Tactical conflict detection and resolution in a 3-D airspace. In Proceedings of the 4th USA/Europe Air Traffic Management R&DSeminar, ATM 2001, Santa Fe, New Mexico, 2001. A long version appears as report NASA/CR-2001-210853 ICASE Report No. 2001-7.
  • [13] G. Dowek, C. Munoz, and V. Carreno. Abstract model of the SATS concept of operations: Initial results and recommendations. Technical Report NASA/TM-2004-213006, NASA Langley Research Center, NASA LaRC,Hampton VA 23681-2199, USA, March 2004.
  • [14] G. Dowek, C. Munoz, and V. Carreno. Provably safe coordinated strategy for distributed conflict resolution. In Proceedings of the AIAA Guidance Navigation, and Control Conference and Exhibit 2005, AIAA-2005-6047, San Francisco, California, 2005.
  • [15] G. Dowek, C. Munoz, and A. Geser. Tactical conflict detection and resolution in a 3-D airspace. Technical Report NASA/CR-2001-210853 ICASE Report No. 2001-7, ICASE-NASA Langley, ICASE Mail Stop 132C, NASA Langley Research Center, Hampton VA 23681-2199, USA, April 2001.
  • [16] M. Daumas, G. Melquiond, and C. Munoz. Guaranteed proofs using interval arithmetic. In Proceedings of the 17th IEEE Symposium on Computer Arithmetic, ARITH-17, Cape Cod, Massachusetts, 2005.
  • [17] A. Geser and C. Munoz. A geometric approach to strategic conflict detection and resolution. In Proceedings of the 21st Digital Avionics Systems Conference, Irvine, CA, 2002.
  • [18] A. Geser, C. Munoz, G. Dowek, and F. Kirchner. Air traffic conflict resolution and recovery. Technical Report ICASE Report No. 2002-12 NASA/CR-2002-211637, ICASE-NASA Langley, ICASE Mail Stop 132C, NASA Langley Research Center, Hampton VA 23681-2199, USA, May 2002.
  • [19] G. Lüttgen, C. Munoz, R. Butler, B. Di Vito, and P. Miner. Towards a customizable PVS. Technical Report NASA/CR-2000-209851 ICASE No. 2000-4, ICASE-NASA Langley, ICASE Mail Stop 132C, NASA Langley Research Center, Hampton VA 23681-2199, USA, January 2000.
  • [20] J. Maddalon, R. Butler, A. Geser, and C. Munoz. Formal verification of a conflict resolution and recovery algorithm. Technical Report NASA/TP-2004-213015, NASA Langley Research Center, NASA LaRC,Hampton VA 23681-2199, USA, April 2004.
  • [21] C. Munoz. ManTa: Un sistema para la implantaci'on certificada y automática de Tipos Abstractos de Datos. Tesis de Magister en Ingenier'ia de Sistemas y Computaci'on. Universidad de los Andes, 1992.
  • [22] C. Munoz. Démonstration automatique dans la logique propositionnelle intuitionniste. Mémoire de DEA d'Informatique Fondamentale, Université Paris 7, 1994.
  • [23] C. Munoz. Un calcul de substitutions pour la représentation de preuves partielles en théorie de types. Th`ese de doctorat, Université Paris 7, 1997. English version available as INRIA research report RR-3309.
  • [24] C. Munoz. Dependent types and explicit substitutions. Mathematical Structures in Computer Science, 11(1):91129, February 2001. A long version appears as report NASA/CR-1999-209722 ICASE No. 99-43.
  • [25] C. Munoz. Proof-term synthesis on dependent-type systems via explicit substitutions. Theoretical Computer Science, 266:407440, 2001. A long version appears as report NASA/CR-1999-209730 ICASE No. 99-47.
  • [26] C. Munoz. Rapid prototyping in PVS. Report NIA Report No. 2003-03, NASA/CR-2003-212418, NIA-NASA Langley, National Institute of Aerospace, Hampton, VA, May 2003.
  • [27] C. Munoz, V. Carreno, G. Dowek, and R.W. Butler. Formal verification of conflict detection algorithms. International Journal on Software Tools for Technology Transfer, 4(3):371380, 2003.
  • [28] C. Munoz, G. Dowek, and V. Carreno. Modeling and verification of an air traffic concept of operations. Software Engineering Notes, 29(4):175182, 2004. A long version appears as report NASA/TM-2004- 213006.
  • [29] C. Munoz and D. Lester. Real number calculations and theorem proving. In Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2005, Oxford, UK, 2005. Accepted for publication.
  • [30] C. Munoz and M. Mayero. Real automation in the field. Technical Report NASA/CR-2001-211271 Interim ICASE Report No. 39, ICASE, Mail Stop 132C, NASA Langley Research Center, Hampton VA 23681-2199, USA, December 2001.
  • [31] C. Munoz and J. Rushby. Structural embeddings: Mechanization with method. In Proceedings of the World Congress on Formal Methods FM'99, volume 1708 of LNCS, pages 452471, Toulouse, France, 1999. A long version appears as report NASA/CR-1999-209360 ICASE No. 99-26.

This page is based on the vitae sent by César Muñoz late in 2005. Please visit César Muñoz's webpages for up-to-date and detailled information.