--- layout: fc_discuss_archives title: Message 104 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] 3rd Workshop on Theorem Proving in Certification



Dear Yannick,

I am not working on this area. But I am interested in formal
verification and would like to join in this workshop. Whether can I
join in?

Thank you very much.

Best Regards
-david

On 14 November 2013 18:18, Yannick Moy <moy at adacore.com> wrote:
> 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).
> --
> Yannick
>
> 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)
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss