Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs |
| |
Authors: | Sylvie Boldo Claude March?? |
| |
Affiliation: | (1) Depto. Inform?tica, Universidade do Minho, Campus de Gualtar, Braga, 4710-057, Portugal;(2) Depto. Inform?tica, Universidade Beira Interior, rua Marques d’Avila e Bolama, Covilh?, 6201-001, Portugal |
| |
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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|