Charles Pecheur
List of Publications


Articles

  1. José Vander Meulen, Charles Pecheur. Efficient Symbolic Model Checking for Process Algebras. Proceedings of 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008), September 2008, L'Aquila, Italy.
  2. Franco Raimondi, Charles Pecheur, Guillaume Brat.  Testing Planning Domains (without Model Checkers).  Third Workshop on Model-Based Testing (MBT 2007), March 31 - April 1, 2007, Braga, Portugal.
  3. Alessio Lomuscio, Charles Pecheur, Franco Raimondi.  Automatic Verification of Knowledge and Time with NuSMV.  In: Twentieth International Joint Conference on Artificial Intelligence (IJCAI-07), January 6-12 2007, Hyderabad, India.
  4. Charles Pecheur, Franco Raimondi. Symbolic Model Checking of Logics with Actions. In: Workshop on Model Checking and Artificial Intelligence (MOCHART), Riva del Garda, Italy, 29 Aug 2006.  Lecture Notes in Artificial Intelligence, vol. 4428, Springer, 2007.
  5. Charles Pecheur, Reid Simmons, Peter Engrand. Formal Verification of Autonomy Models: From Livingstone to SMV. In: Rouff, C.; Hinchey, M.; Rash, J.; Truszkowski, W.; Gordon-Spears, D. (Eds.), Agent Technology from a Formal Perspective, NASA Monographs in Systems and Software Engineering, Springer Verlag, 2006.
  6. Franco Raimondi, Charles Pecheur, Alessio Lomuscio. Applications of model checking for multi-agent systems: verification of diagnosability and recoverability. In: Proceedings of Concurrencey Specification and Programming (CSP 2005), Ruciane-Nida, Poland, Sep 2005.
  7. Tim Menzies and Charles Pecheur. Verification and Validation and Artificial Intelligence. In: M. Zelkowitz, Ed., Advances in Computers, vol. 65, 2005, Elsevier.
  8. Tony Lindsey and Charles Pecheur.  Simulation-Based Verification of Autonomous Controllers with Livingstone PathFinder. In: Proceedings of the Tenth International Conference on Tools And Algorithms For The Construction And Analysis Of Systems (TACAS'04), Barcelona, Spain, Mar-Apr 2004. Lecture Notes in Computer Science, vol. 2988, Springer Verlag.
  9. A.E. Lindsey and Charles Pecheur.  Simulation-Based Verification of Livingstone Applications.  Short paper, Workshop on Model-Checking for Dependable Software-Intensive Systems, San Francisco, June 2003.
  10. Alessandro Cimatti, Charles Pecheur, Roberto Cavada.  Formal Verification of Diagnosability via Symbolic Model Checking. Proceedings of IJCAI'03, Acapulco, Mexico, August 2003.
  11. Stacy Nelson, Charles Pecheur. Formal Verification of a Next-Generation Space Shuttle. In: Second Goddard Workshop on Formal Aspects of Agent-Based Systems (FAABS II), Greenbelt, MD, October 2002. Lecture Notes in Computer Science, vol. 2699, Springer Verlag.
  12. Charles Pecheur, Alessandro Cimatti. Formal Verification of Diagnosability via Symbolic Model Checking. Workshop on Model Checking and Artificial Intelligence (MoChArt-2002), Lyon, France, July 22/23, 2002.
  13. Steven Brown, Charles Pecheur. Model-Based Verification of Diagnostic Systems. Proceedings of JANNAF Joint Meeting, Destin, FL, April 8-12, 2002.
  14.  Reid Simmons, Charles Pecheur, Grama Srinivasan. Towards Automatic Verification of Autonomous Systems. In: Proceedings of the 2000 IEEE/RSJ International Conference on Intelligent Robots and Systems, IEEE, 2000.
  15. Klaus Havelund, Mike Lowry, SeungJoon Park, Charles Pecheur, John Penix, Willem Visser, Jon L. White. Formal Analysis of the Remote Agent Before and After Flight. In: Proceedings of 5th NASA Langley Formal Methods Workshop, Williamsburg, Virginia, 13-15 June 2000.
  16. Charles Pecheur, Reid Simmons. From Livingstone to SMV: Formal Verification for Autonomous Spacecrafts. In:Proceedings of First Goddard Workshop on Formal Approaches to Agent-Based Systems, NASA Goddard, April 5-7, 2000. Lecture Notes in Computer Science, vol. 1871, Springer Verlag.
  17. Reid Simmons, Charles Pecheur. Automating Model Checking for Autonomous Systems. Proceedings of AAAI Spring Symposium on Real-Time Autonomous Systems, Stanford, March 20-22, 2000.
  18. Daniel Clancy, William Larson, Charles Pecheur, Peter Engrand, Charles Goodrich. Autonomous Control of an in-Situ Propellant Production Plant. In: Proceedings of the Technology 2009 National Conference, Miami Beach, FL, November 1-3, 1999.
  19. Anthony R. Gross, K. R. Sridhar, William E. Larson, Daniel J. Clancy, Charles Pecheur, and Geoffrey A. Briggs. Information Technology and Control Needs for In-Situ Resource Utilization. In: Proceedings of the 50th IAF Congress, Amsterdam, 4-8 October 1999.
  20. Charles Pecheur. Advanced Modelling and Verification Techniques Applied to a Cluster File System. In: Proceedings of the 14th IEEE International Conference on Automated Software Engineering, Cocoa Beach, Florida, October 1999. Extended version in: INRIA Research Report RR-3416, May 1998.
  21. John Penix, Charles Pecheur and Klaus Havelund. Using Model Checking to Validate AI Planner Domain Models. In: Proceedings of the 23rd Annual Software Engineering Workshop, NASA Goddard, December, 1998.
  22. Charles Pecheur. Specification and Validation of the CO4 distributed knowledge system using LOTOS. in: Proceedings of the 12th IEEE International Conference on Automated Software Engineering, Incline Village, Nevada, November 1997. Extended version in: INRIA Research Report RR-3259, September 1997.
  23. Hubert Garavel, Mark Jorgensen, Radu Mateescu, Charles Pecheur, Mihaela Sighireanu, Bruno Vivien. CADP'97 -- Status, Applications and Perspectives.In:  Ignac Lovrek (ed.), Proceedings of the 2nd COST 247 International Workshop on Applied Formal Methods in System Design (Zagreb, Croatia), June 1997.
  24. G. Leduc, O. Bonaventure, L. Leonard, E. Koerner, C. Pecheur. Model-Based Verification of a Security Protocol for the Conditional Access to Services. Formal Methods in System Design, Vol. 14, nr 2, March 1999, pp 171-191.
  25. G. Leduc , O. Bonaventure, E. Koerner, L. Léonard, C. Pecheur, D. Zanetti. Specification and verification of a TTP protocol for the conditional access to services. In: Proceedings of 12th J. Cartier Workshop. Formal Methods and their Applications: Telecommunications, VLSI and Real-Time Computerized Control System, Montreal, Canada, 2-4 Oct. '96.
  26. Charles Pecheur. VLib: Infinite virtual libraries for LOTOS. In: A. Danthine, G. Leduc, P. Wolper (eds.) Proceedings of the IFIP TC6/WG6.1 Thirteenth International Symposium on Protocol Specification, Testing and Verification, Liège, Belgium, 25-28 May, 1993 Elsevier Science Publishers BV (North Holland), 1993, pp 29-44.
  27. Charles Pecheur. Using LOTOS for Specifying the CHORUS Distributed Operating System Kernel. In: Computer Communications Vol. 15, nr 2, March 1992, pp 93-102.
  28. Charles Pecheur. Spécification de Systèmes d'Exploitation en LOTOS: l'Expérience CHORUS. In: CFIP'91 Ingénierie des Protocoles, Omar Rafiq (ed.), Hermès, Paris, 1991, pp. 405-424.

PhD Thesis

Charles Pecheur. Improving the Specification of Data Types in LOTOS. Doctorate Thesis, Collection des Publications de la FSA No. 171, University of Liège, 1996. Abstract.

Selected Technical Reports

  1. Tony Lindsey, Charles Pecheur. Simulation-Based Verification of a Propulsion Feed Subsystem via Livingstone PathFinder. RIACS Technical Report 03.11, RIACS, USRA, September 2003.
  2. Cavada, Roberto and Pecheur, Charles. Practical Formal Verification of Diagnosability of Large Models via Symbolic Model Checking. Technical Report TR03.03, RIACS, USRA, January 2003.
  3. Stacy Nelson, Charles Pecheur. NASA processes/methods applicable to IVHM V&V. Project report, 2nd Gen RLV Program, NRA 8-30/TA-5/Northrop Grumman/ARC Task 10. Oct 2001. Available as NASA/CR-2002-211401, April 2002.
  4. Stacy Nelson, Charles Pecheur. Methods for V&V of IVHM intelligent systems. Project report, 2nd Gen RLV Program, NRA 8-30/TA-5/Northrop Grumman/ARC Task 10. Jan 2002. Available as NASA/CR-2002-211402, April 2002.
  5. Stacy Nelson, Charles Pecheur. Diagnostic Model V&V Plan/Methods for DME. Project report, 2nd Gen RLV Program, NRA 8-30/TA-5/Northrop Grumman/ARC Task 10. Jan 2002. Available as NASA/CR-2002-211403, April 2002.
  6. Charles Pecheur. Verification and Validation of Autonomy Software at NASA. NASA/TM 2000-209602, August 2000.
  7. Charles Pecheur. A Proposal for Data Types in E-LOTOS. Annex H of: Working Draft on Enhancements to LOTOS, ISO JTC1/SC21/WG1/N1349, November 1994.
  8. Charles Pecheur. APERO Language Reference Version 1.0. EC-CA Project 0001:76099 Eucalyptus, EUCA/ULG/05, University of Liege, Systèmes et Automatique, February 1994.
  9. Charles Pecheur. APERO Tools User's Guide Version 2.0. EC-CA Project 0001:76099 Eucalyptus, EUCA/ULG/06, University of Liege, Systèmes et Automatique, February 1994.

Other Publications

  1. Charles Pecheur.  Verification of Embedded Software: From Mars to Actions.  Invited talk (abstract),  FMICS 2007, Berlin, Germany, July 2007. Lecture Notes in Computer Sciences, vol. 4916, Springer, 2008.
  2. Charles Pecheur. Verification of Intelligent Control Software. Presented at ASTRA'06, Noordwijk, Netherlands, November 2006.
  3. Charles Pecheur, Willem Visser, Reid Simmons.  RIACS Workshop on the Verification and Validation of Autonomous and Adaptive Systems. Conference report, AI Magazine, Fall 2001. Also available as NASA/TM-2001-210927, August 2001.

Tutorials

  1. Stacy Nelson, Michael Whalen, Charles Pecheur. From Research to Industry: The Role of Software Engineering Standards. Tutorial presented at the ASE'02 conference, Edinburgh, UK, September 2002.
  2. Charles Pecheur, Willem Visser. Model Checking for Software. Tutorial presented at the ASE'00 conference, Grenoble, France, 12 September 2000.
  3. Klaus Havelund, Charles Pecheur, Reid Simmons, Willem Visser. Software Model Checking Tools and Trends at NASA. Tutorial presented at Lfm 2000, Williamsburg, Virginia, June 2000.