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

Sylvie Boldo 1, 2
1 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. To achieve this high level of confidence on C programs, we use a chain of tools: Frama-C, its Jessie plugin, Why and Coq. This requires the C program to be annotated: this means that each function must be precisely specified, and we will prove the correctness of the program by proving both that it meets its specifications and that it does not fail. Examples will be given to illustrate the features of this approach.
Document type :
Conference papers
NSV-3: Third International Workshop on Numerical Software Verification, Jul 2010, Edinburgh, Scotland, United Kingdom. 2010
Liste complète des métadonnées


https://hal.inria.fr/inria-00534400
Contributor : Sylvie Boldo <>
Submitted on : Tuesday, November 9, 2010 - 3:10:52 PM
Last modification on : Thursday, February 9, 2017 - 3:54:57 PM
Document(s) archivé(s) le : Friday, October 26, 2012 - 3:20:34 PM

File

article.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00534400, version 1

Collections

Citation

Sylvie Boldo. Formal verification of numerical programs: from C annotated programs to Coq proofs. NSV-3: Third International Workshop on Numerical Software Verification, Jul 2010, Edinburgh, Scotland, United Kingdom. 2010. <inria-00534400>

Share

Metrics

Record views

318

Document downloads

101