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

  • Subject: [Frama-c-discuss] French slides to present Frama-C, value analysis and Jessie
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Tue, 01 Feb 2011 21:04:57 +0100
  • In-reply-to: <1296557709.1660.53.camel@iti27>
  • References: <AANLkTi=OSq-Pbw8qwyLy-EoDfY0dOPa2ucV+6RRXtrVQ@mail.gmail.com> <75024FAF-DEA9-4F87-8B45-ADC3475A194E@cea.fr> <AANLkTikQfC8Xz4x1CMP=XES-e7a=t-QB8WG1R5Xhex75@mail.gmail.com> <1296557709.1660.53.camel@iti27>
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