Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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