Automating the Verification of Floating-Point Programs

Clément Fumex 1, 2, 3 Claude Marché 1, 2 Yannick Moy 3
1 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : In the context of deductive program verification, handling floating-point computations is challenging. The level of proof success and proof automation highly depends on the way the floating-point operations are interpreted in the logic supported by back-end provers. We address this challenge by combining multiple techniques to separately prove different parts of the desired properties. We use abstract interpretation to compute numerical bounds of expressions, and we use multiple automated provers, relying on different strategies for representing floating-point computations. One of these strategies is based on the native support for floating-point arithmetic recently added in the SMT-LIB standard. Our approach is implemented in the Why3 environment and its front-end SPARK 2014 for the development of safety-critical Ada programs. It is validated experimentally on several examples originating from industrial use of SPARK 2014.
Type de document :
Communication dans un congrès
Andrei Paskevich and Thomas Wies. 9th Working Conference on Verified Software: Theories, Tools and Experiments, Jul 2017, Heidelberg, Germany. Springer, 9th Working Conference on Verified Software: Theories, Tools and Experiments. <http://vstte17.lri.fr/>
Liste complète des métadonnées


https://hal.inria.fr/hal-01534533
Contributeur : Claude Marché <>
Soumis le : mercredi 7 juin 2017 - 16:54:38
Dernière modification le : jeudi 15 juin 2017 - 09:09:43

Fichier

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

Identifiants

  • HAL Id : hal-01534533, version 1

Citation

Clément Fumex, Claude Marché, Yannick Moy. Automating the Verification of Floating-Point Programs. Andrei Paskevich and Thomas Wies. 9th Working Conference on Verified Software: Theories, Tools and Experiments, Jul 2017, Heidelberg, Germany. Springer, 9th Working Conference on Verified Software: Theories, Tools and Experiments. <http://vstte17.lri.fr/>. <hal-01534533>

Partager

Métriques

Consultations de
la notice

143

Téléchargements du document

68