Third Workshop on Theorem Proving in Certification (TPC3)

Time: Monday December 9 and Tuesday December 10, 2013.

Place: Rooms SW00-01 of the University of Cambridge Computer Laboratory (directions).

Scientific program: Jeff Joyce (Critical Systems Labs), Lee Pike (Galois)
Local organisation: Mike Gordon (Computer Laboratory)


This is the third in a series of workshops that examines how the use of machine-assisted theorem proving (interactive and automatic) as a method for increasing assurance that implementations meet specifications. Earlier workshops in December 2010 (web-page) and December 2011 (web-page) brought experts in theorem-proving methodology together with experts in certification including representation from the aerospace, security and defense sectors.

The aim of this third workshop is to develop a "strawman" standard that could be used by certification authorities to decide on the extent to which verification results produced by means of theorem-proving may be used instead of some portion of the test-based verification results conventionally required to certify critical systems (background).

In the second workshop a simplified "certification standard" was referred to by some participants when explaining how their approach might be used to support the overall objectives of certification. This simplified standard would, at most, be a starting point for discussion. The strawman that we hope will be the end result of the workshop might be something completely different than the simplified certification standard.

A portion of the workshop schedule was reserved for presentations on solutions to the "Nose Gear Problem" motivating example. Presentations 1 and 2 (see below) addressed this. The rest of the two-day workshop was spent on contributed talks and discussions of the strawman standard.

Presentations were given by Philippe Baufreton (Sagem), Yannick Moy (AdaCore), Colin O'Halloran (D-RisQ), Julien Schmaltz (OU Netherlands) and Jeff Joyce (CSL).

The subtopic coordinators are:

      Subtopic 1: Nick Tudor
      Subtopic 2: Yannick Moy
      Subtopic 3: Jeff Joyce
      Subtopic 4: Lee Pike
      Subtopic 5: Yannick Moy (representing Johannes Kanig)
      Subtopic 6: Colin O'Halloran


      Day 1 (December 9, 2013)
      09:00 Coffee, gather
      09:30 Introductions, opening remarks
      10:00 Presentation #1: Yannick Moy (AdaCore)
      11:00 Break
      11:30 Subtopic 1,6 full-group discussion
      12:00 Lunch (provided)
      13:30 Subtopic 2 full-group discussion
      14:00 Subtopic 3 full-group discussion (Jeff's Presentation)
      14:30 Presentation #2: Colin O'Halloran (D-RisQ)
      15:00 Presentation #3: Julien Schmaltz (OU Netherlands)
      15:30 Tea
      16:00 Subtopic 4 full-group discussion
      16:30 Subtopic 5 full-group discussion
      17:00 Plan for day 2
      19:30 Dinner in the Riverside Restaurant

      Day 2 (December 10, 2013)

      09:00 Coffee, gather
      09:30 Presentation #4: Philippe Baufreton (Sagem)
      10:00 Presentation #5: Jeff Joyce (CSL)
      10:30 Break
      11:00 Breakouts: 2,3
      12:00 Lunch (provided)
      13:30 Breakouts: 4,5
      14:30 Group summary
      15:30 Tea
      16:00 Recap, post-workshop planning

Links and resources

Maintained by Mike Gordon.
This page last updated on Wed Jan 15 2014 (to fix broken links).