Proving Floating-Point Numerical Programs by Analysis of their Assembly Code
Résumé
We present an approach for proving behavioral properties of numerical programs by analyzing their compiled assembly code. We focus on the issues and traps that may arise on floating-point computations. Direct analysis of the assembly code allows to accurately take into account architecture- or compiler-dependent features such as the possible use of extended precision registers. The approach is implemented on top of the generic \Why platform for deductive verification, which allows us to perform experiments where proofs are discharged by combining several back-end automatic provers.
Nous décrivons une nouvelle approche pour prouver des propriétés du comportement des programmes numériques en analysant leur code assembleur compilé. Nous mettons l'accent sur les enjeux et les pièges qui peuvent survenir lors des calculs en virgule flottante. L'analyse directe du code assembleur permet de prendre en compte de façon précise l'architecture et le compilateur, par exemple l'utilisation de registres en précision flottante étendue. Un prototype est implanté au-dessus de la plate-forme générique \Why plate-forme pour la vérification déductive. Nous présentons des expérimentations où les preuves sont effectuées par une combinaison de plusieurs prouveurs automatiques.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...