Automated Verification of Floating-Point Computations in Ada Programs - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2017

Automated Verification of Floating-Point Computations in Ada Programs

Vérification automatique de programmes Ada effectuant des calculs en virgule flottante

(1, 2) , (1, 2) , (3)
1
2
3

Abstract

In critical software systems like the ones related to transport and defense, it is common to perform numerical computations implemented using floating-point arithmetic. Safety conditions for such systems typically require strong guarantees on the functional behavior of the performed computations. Automatically verifying that these guarantees are fulfilled is thus desirable. Deductive program verification is a promising approach for verifying that a given code fulfills a functional specification, with a very high level of confidence. Yet, formally proving correct a program performing floating-point computations remains a challenge, because floating-point arithmetic is not easily handled by automated theorem provers. We address this challenge by combining multiple techniques to separately prove parts of the desired proper- ties. On the one hand, abstract interpretation computes numerical bounds for expressions that appear either in the original program, or in the ghost code added to instrument the program. On the other hand, we gen- erate verification conditions for different automated provers, relying on different strategies for representing floating-point computations. Among these strategies, we try to exploit the native support for floating-point arithmetic recently added in the SMT-LIB standard. Our approach is partly implemented in the Why3 environment for deductive program verification, and partly implemented in its front-end environment SPARK for the development of safety-critical Ada programs. We report on several examples and case studies used to validate our approach experimentally.
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.
Fichier principal
Vignette du fichier
RR-9060.pdf (720.61 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01511183 , version 1 (20-04-2017)

Licence

Attribution - ShareAlike - CC BY 4.0

Identifiers

  • HAL Id : hal-01511183 , version 1

Cite

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⟩
446 View
570 Download

Share

Gmail Facebook Twitter LinkedIn More