Formal verification of numerical programs: from C annotated programs to mechanical proofs

Sylvie Boldo 1, 2 Claude Marché 1, 2
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : Numerical programs may require a high level of guarantee. This can be achieved by applying formal methods, such as machine-checked proofs. But these tools handle mathematical theorems while we are interested in C code, in which numerical computations are performed using floating-point arithmetic, whereas proof tools typically handle exact real arithmetic. To achieve this high level of confidence on C programs, we use a chain of tools: Frama-C, its Jessie plugin, Why and provers among Coq, Gappa, Alt-Ergo, CVC3 and Z3. This approach requires the C program to be annotated: each function must be precisely specified, and we prove the correctness of the program by proving both that it meets its specifications and that no runtime error may occur. The purpose of this paper is to illustrate, on various examples, the features of this approach.
Type de document :
Article dans une revue
Mathematics in Computer Science, Springer, 2011, 5, pp.377-393
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00777605
Contributeur : Claude Marché <>
Soumis le : jeudi 17 janvier 2013 - 16:55:15
Dernière modification le : jeudi 5 avril 2018 - 12:30:08
Document(s) archivé(s) le : jeudi 18 avril 2013 - 04:01:56

Fichier

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

Identifiants

  • HAL Id : hal-00777605, version 1

Collections

Citation

Sylvie Boldo, Claude Marché. Formal verification of numerical programs: from C annotated programs to mechanical proofs. Mathematics in Computer Science, Springer, 2011, 5, pp.377-393. 〈hal-00777605〉

Partager

Métriques

Consultations de la notice

305

Téléchargements de fichiers

353