--- layout: fc_discuss_archives title: Message 104 from Frama-C-discuss on November 2013 ---
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