--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on February 2011 ---
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