Multi-prover verification of floating-point programs

Ali Ayad 1, 2 Claude Marché 3
3 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
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
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00534333
Contributeur : Claude Marché <>
Soumis le : mercredi 10 novembre 2010 - 14:00:59
Dernière modification le : lundi 24 septembre 2018 - 11:34:02
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 15:21:07

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00534333, version 1

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

419

Téléchargements de fichiers

227