Formal Verification of Numerical Programs:From C Annotated Programs to Mechanical Proofs

摘要

Numerical programs may require a high level of guarantee. This can be achieved by applying formalmethods, such as machine-checked proofs. But these tools handle mathematical theorems while we are interestedin C code, in which numerical computations are performed using floating-point arithmetic, whereas proof toolstypically handle exact real arithmetic. To achieve this high level of confidence on C programs, we use a chain oftools: Frama-C, its Jessie plugin, Why and provers among Coq, Gappa, Alt-Ergo, CVC3 and Z3. This approachrequires the C program to be annotated: each function must be precisely specified, and we prove the correctness ofthe program by proving both that it meets its specifications and that no runtime error may occur. The purpose ofthis paper is to illustrate, on various examples, the features of this approach.