[Why3-club] 3rd Workshop on Theorem Proving in Certification

Yannick Moy moy at adacore.com
Thu Nov 14 19:18:36 CET 2013

The invitation below may be of interest to other members of this list interested in formal verification and certification. I will participate and present the solution AdaCore has been working on for the NoseGear challenge, using in particular the SPARK language and formal verification tools (based on Why3 and the prover Alt-Ergo).

I participated in the previous edition two years ago, and found it very productive. The goal this year, besides comparing solutions to the NoseGear challenge, is to work on a strawman standard for the use of formal methods in a certification standard. Some certification standards like EN 50128 for railway have since long allowed the use of formal methods for addressing verification activities. Others like DO-178C for avionics have just started on this path. I view this workshop as an opportunity to influence how these permissions are interpreted by certification authorities and companies submitted to certification.

If interested in participating, please contact one of the co-organizers for a formal invitation (Jeff Joyce, Lee Pike or Mike Gordon). 

> Dear participant to the Workshop on Theorem Proving in Certification,
> A few months ago you expressed an interest our plans for an informal
> collaboration to develop a "strawman" standard for using theorem
> proving in certification.
> Our original plan had been for this collaboration to start several
> months ago with a workshop in December to review and improve a draft
> version of this strawman standard.  It has taken much longer than we
> had expected to get this initiative off the ground, but nevertheless,
> we hope that you are still interested in participating in this
> collaboration.  In particular, we are writing to invite you to
> participate in workshop in Cambridge, UK December 9-10 which will
> serve as the launch of this collaborative effort.
> To help structure our collaborative efforts during the workshop, we have
> identified six sub-topics that we suggest should be addressed by the
> strawman standard.  Our agenda will be partially driven by these
> six sub-topics, e.g., parallel break-out sessions focused on individual
> sub-topics.  In addition to exchanging knowledge and expert opinion
> about the concepts underlying the use of theorem-proving in certification,
> we hope the workshop will result in a working plan for development of the
> strawman over the next year.
> A substantial portion of the agenda will be reserved for focused
> discussion on the strawman standard and, hopefully, some initial
> drafting of text for this document.  We have also tentatively reserved
> time in the workshop for short 20-minute presentations by participants
> that ideally, will motivate and guide this collaborative effort.
> In spite of the relatively short notice, we hope that you will
> consider coming to Cambridge for this workshop on December 9-10.  The
> workshop will be held at the University of Cambridge Computer
> Laboratory in the William Gates Building on JJ Thompson Rd.  Please see
> http://www.cl.cam.ac.uk/~mjcg/FMStandardsWorkshop for additional 
> information.
> To help us make arrangements for this workshop, please reply to this
> email to let us to know if you would like to participate in the
> workshop.  If you are not yet sure, it would be helpful to know in
> advance if you are considering this possibility.  If you are
> interested in making a presentation at the workshop, please send us an
> abstract for consideration.  Preference will be given to presentations
> that speak to one or more of the sub-topics identified in the above
> link.
> Best regards,
> Jeff Joyce (Critical Systems Labs),
> Lee Pike (Galois)
> Mike Gordon (Computer Laboratory)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20131114/5ebf5e8d/attachment.html>

More information about the Why3-club mailing list