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] French slides to present Frama-C, value analysis and Jessie

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>