Paper Info
Title
Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs.
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.
Year
DOI
Venue
2011
10.1007/s11786-011-0099-9
Mathematics in Computer Science
Keywords
Field
DocType
Floating-point arithmetic, C program, Formal specification, Automated reasoning
Automated reasoning,Programming language,Computer science,Floating point,Correctness,Formal specification,Theoretical computer science,Mathematical proof,Plug-in,Formal methods,Formal verification
Journal
Volume
Issue
ISSN
5
4
1661-8270
Citations 
PageRank 
References 
11
0.59
19
Authors
2
Name
Order
Citations
PageRank
Sylvie Boldo129226.85
Claude Marché281447.43