--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on January 2019 ---
Le 21/01/2019 à 17:20, Rafael Bachmann a écrit : > Apart from these (I may be wrong, usually am), I had difficulties finding > good documentation regarding floating point numbers. > This habilitation:https://hal.inria.fr/tel-01089643/document contains many > very good examples, none of which I can reproduce (the author uses Coq > sometimes, but in other cases gappa suffices). On my machine, the > verification simply fails. Might something be wrong with my Frama-C > installation? I would say that the first mistake could be that you tried those using the WP plug-in, whereas these examples were proved using Jessie instead. I believe that they should be reproducible even with recent versions of Frama-C. For the proper source codes and proof sessions you may look at http://toccata.lri.fr/gallery/fp.en.html and https://www.lri.fr/~sboldo/research.html For more documentation: see also @book{BM17, title = {Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the {Coq} System}, author = {Boldo, Sylvie and Melquiond, Guillaume}, hal = {https://hal.inria.fr/hal-01632617}, publisher = {ISTE Press - Elsevier}, year = 2017, month = dec }