Automated Verification of Floating-Point Computations in Ada Programs

Clément Fumex 1, 2 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
Résumé : Dans les logiciels critiques comme ceux liés aux transports et à la défense, il est courant d’effectuer des calculs numériques implémentés à l’aide de l’arithmétique à virgule flottante. Les exigences de sûreté de ces systèmes requièrent généralement des garanties fortes sur le comportement fonctionnel des calculs ainsi exécutés. Vérifier automatiquement que ces garanties sont remplies est donc souhaitable. La vérification déductive des programmes est une approche prometteuse pour vérifier formellement qu’un code donné satisfait une spécification fonctionnelle, avec un haut niveau de confiance. Néanmoins, prouver formellement qu’un programme qui effectue des calculs en virgule flottante est correct reste un défi, car l’arithmétique à virgule flottante n’est pas facilement traitée par les prouveurs automatiques. Nous abordons ce défi en combinant plusieurs techniques pour prouver séparément chaque partie des propriétés souhaitées. D’une part, l’interprétation abstraite calcule les bornes numériques pour les expressions qui apparaissent dans le programme d’origine, ou dans le code fantôme ajouté pour instrumenter le code. D’autre part, nous générons des obligations de preuve pour plusieurs prouveurs automatiques différents, s’appuyant sur différentes représentations des calculs en virgule flottante. En particulier, nous exploitons le support natif de l’arithmétique en virgule flottante récemment apparue dans le standard SMT-LIB. Notre approche est mise en oeuvre en partie dans la boîte à outils générique Why3 pour la vérification déductive, et en partie dans l’environnement SPARK pour le développement de programmes Ada critiques. Nous présentons des exemples et études de cas qui ont été utilisées pour valider notre approche expérimentalement.
Type de document :
Rapport
[Research Report] RR-9060, Inria Saclay Ile de France. 2017, pp.53
Liste complète des métadonnées


https://hal.inria.fr/hal-01511183
Contributeur : Claude Marché <>
Soumis le : jeudi 20 avril 2017 - 15:01:41
Dernière modification le : jeudi 15 juin 2017 - 09:09:29

Fichier

RR-9060.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Partage selon les Conditions Initiales 4.0 International License

Identifiants

  • HAL Id : hal-01511183, version 1

Citation

Clément Fumex, Claude Marché, Yannick Moy. Automated Verification of Floating-Point Computations in Ada Programs. [Research Report] RR-9060, Inria Saclay Ile de France. 2017, pp.53. <hal-01511183>

Partager

Métriques

Consultations de
la notice

250

Téléchargements du document

79