Formal verification of numerical programs: from C annotated programs to Coq proofs - Archive ouverte HAL Access content directly
Conference Papers Year : 2010

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

(1, 2)
1
2

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.
Fichier principal
Vignette du fichier
article.pdf (208.88 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00534400 , version 1 (09-11-2010)

Identifiers

  • HAL Id : inria-00534400 , version 1

Cite

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⟩
225 View
181 Download

Share

Gmail Facebook Twitter LinkedIn More