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