Skip to Main content Skip to Navigation
Conference papers

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
Complete list of metadata

Cited literature [1 references]  Display  Hide  Download
Contributor : Sylvie Boldo Connect in order to contact the contributor
Submitted on : Tuesday, November 9, 2010 - 3:10:52 PM
Last modification on : Thursday, July 8, 2021 - 3:49:24 AM
Long-term archiving on: : Friday, October 26, 2012 - 3:20:34 PM


Files produced by the author(s)


  • HAL Id : inria-00534400, version 1



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. ⟨inria-00534400⟩



Les métriques sont temporairement indisponibles