Abstract : In the context of deductive program verification, supporting floatingpoint computations is tricky.We propose an expressive language to formally specify behavioral properties of such programs. We give a first-order axiomatization of floating-point operations which allows to reduce verification to checking the validity of logic formulas, in a suitable form for a large class of provers including SMT solvers and interactive proof assistants. Experiments using the Frama-C platform for static analysis of C code are presented.
Type de document :
Communication dans un congrès
Jürgen Giesl and Reiner Hähnle. Fifth International Joint Conference on Automated Reasoning, Jul 2010, Edinburgh, United Kingdom. Springer Verlag, 6173, 2010, Lecture Notes in Artificial Intelligence
https://hal.inria.fr/inria-00534333
Contributeur : Claude Marché
<>
Soumis le : mercredi 10 novembre 2010 - 14:00:59
Dernière modification le : jeudi 5 avril 2018 - 12:30:08
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 15:21:07
Ali Ayad, Claude Marché. Multi-prover verification of floating-point programs. Jürgen Giesl and Reiner Hähnle. Fifth International Joint Conference on Automated Reasoning, Jul 2010, Edinburgh, United Kingdom. Springer Verlag, 6173, 2010, Lecture Notes in Artificial Intelligence. 〈inria-00534333〉
