Charles Pecheur
Presentation Slides



Model Checking for Software. Tutorial presented at MoVES WP 5-6-7 Meeting, Brussels, Belgium, 17 June 2008.  Revised version of ASE '00 tutorial (see below).

Verification of Embedded Software: from Mars to Actions. Invited talk at FMICS '07, Berlin, Germany, July 2007.

Symbolic Model Checking of Logics with Actions. Article presented at MOCHART '06, Riva Del Garda, Italy, August 2006.

Guided Simulation of Autonomous Controllers. Presentation at Dagtstuhl Seminar on Directed Model Checking, Dagstuhl, Germany, May 2006.

Verification of Intelligent Controllers using Model Checking. Presentation at IFIP WG 10.4 Winter Meeting, Tucson, AZ, February 2006.

Verification and Validation for ISHM. Data sheet for Industry Partnership Forum, NASA Ames, July 2004.

Verification of Diagnosability using Model Checking (and why NASA cares). Presentation at Kestrel Institute, July 2004.

Verification of Diagnosability. Presentation and demonstration at Jet Propulsion Laboratory, April 2004.

Simulation-Based Verification of Autonomous Controllers with Livingstone PathFinder. Article presented at TACAS'04, Barcelona, Spain, Mar-Apr 2004 (with Tony Lindsey).

Verification of Intelligent Software and Verification and Validation of Integrated Vehicle  Health Management. Presentation and demonstration to different IVHM R&D Teams, September-October 2003. [Note: some semi-transparent objects are missing in the PDF rendering. My apologies for that.]

Verification of Autonomy Software. Poster presented at NASA Ames code IC Open House, January 2003.  (The same as separate slides.)

Formal Verification for a Next-Generation Space Shuttle. Article presented at Second FAABS Workshop, Greenbelt, MD, October 2002 (with Stacy Nelson).

Formal Verification of Diagnosability via Symbolic Model Checking. Article presented at MoChArt 2002 Workshop, Lyon, France, July 23, 2002 (with Alessandro Cimatti).

Symbolic Model Checking of Domain Models for Autonomous Spacecrafts. Presentation at University of Liège, Belgium, 12 November 2001.

Symbolic Model Checking of Domain Models for Autonomous Spacecrafts. Presentation at the Dagstuhl Seminar: Exploration of Large State Spaces, Dagstuhl, Germany, 8 November 2001.

RIACS Workshop on the Verification and Validation of Autonomous and Adaptive Systems (Asilomar, December 2000). Report presented as a RIACS Seminar at NASA Ames, Moffett Field, California, February 2001 (with Willem Visser).

Verification of Intelligent Software. Presentation at NASA Kennedy Space Center, Florida, November 2000. Also presented at San Jose State University, 17 October 2001.

Model Checking for Software. Tutorial presented at the ASE'00 conference, Grenoble, France, 12 September 2000 (with Willem Visser).

Software Model Checking Tools and Trends at NASA. Tutorial presented at Lfm 2000, Williamsburg, Virginia, June 2000 (with Klaus Havelund, Reid Simmons and Willem Visser).

From Livingstone to SMV: Formal Verification for Autonomous Spacecrafts . Article presented at FAABS 2000, Greenbelt, Maryland, April 2000.

Model Checking for Autonomy Software. Presented as a RIACS Seminar at NASA Ames, Moffett Field, California, November 1999.

Advanced Modelling and Verification Techniques Applied to a Cluster File System . Article presented at ASE'99, Cocoa Beach, Florida, October 1999.

Formal Verification of Autonomous Systems. Presented at Florida Institute of Technology, Melbourne, Florida, October 1999.

Towards Verification of Autonomy Software. Presentation at 2nd Assurance Technology Conference, Cleveland, Ohio, May 1999.