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
Schedule:
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