--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on February 2011 ---
Hi, Is it possible to put up slides in English as well? Vijay From: Claude Marche <Claude.Marche at inria.fr> To: frama-c-discuss at lists.gforge.inria.fr Date: 02/02/2011 01:35 AM Subject: Re: [Frama-c-discuss] French slides to present Frama-C, value analysis and Jessie Sent by: frama-c-discuss-bounces at lists.gforge.inria.fr Dear All, On 01/02/2011 11:55, Boris Hollas wrote: >> One of the attendee followed a lesson on code proof using a functional >> approach and PVS powerful tactics made by a researcher at INRIA Rennes >> (Thomas Genet) and told the approach was more powerful and simple. I >> answered that the discussion between the two approaches is still >> on-going. :-) > > Do you know more about this approach? > My two cents in this interesting discussion: PVS is designed for the proof of purely functional (i.e. without side effects at all) algorithms. It also involves only mathematical, unbounded, integers and real numbers, although some support for machine integers and floating-point numbers is available using specific libraries. Jessie/Why is in principle able to output VCs in PVS syntax for proving them inside the PVS environment. Although I'm afraid that it was not used for some time and might need some update. Let me cite the following recent paper about the KB3D case study from NASA, and a comparison between the pure PVS code and its C equivalent. Sylvie Boldo and Thi Minh Tuyen Nguyen. Hardware-independent proofs of numerical programs. In C?sar Mu noz, editor, Proceedings of the Second NASA Formal Methods Symposium, NASA Conference Publication, pages 14-23, Washington D.C., USA, April 2010. http://hal.inria.fr/inria-00534410/en/ - Claude _______________________________________________ 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 =====-----=====-----===== Notice: The information contained in this e-mail message and/or attachments to it may contain confidential or privileged information. If you are not the intended recipient, any dissemination, use, review, distribution, printing or copying of the information contained in this e-mail message and/or attachments to it are strictly prohibited. If you have received this communication in error, please notify us by reply e-mail or telephone and immediately and permanently delete the message and any attachments. Thank you -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110202/373f7437/attachment.htm>