Name
Abstract | ||
|---|---|---|
Many numerical problems require a higher computing precision than the one offered by standard floating-point formats. A common way of extending the precision is to use floating-point expansions. As the problems may be critical and as the algorithms used have very complex proofs (many sub-cases), a formal guarantee of correctness is a wish that can now be fulfilled, using interactive theorem proving. In this article we give a formal proof in Coq for one of the algorithms used as a basic brick when computing with floating-point expansions, the renormalization, which is usually applied after each operation. It is a critical step needed to ensure that the resulted expansion has the same property as the input one, and is more "compressed". The formal proof uncovered several gaps in the pen-and-paper proof and gives the algorithm a very high level of guarantee. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1007/978-3-319-66107-0_7 | INTERACTIVE THEOREM PROVING (ITP 2017) |
Keywords | Field | DocType |
Floating-point arithmetic, Floating-point expansions, Multiple-precision arithmetic, Formal proof, Coq | Renormalization,Discrete mathematics,Arbitrary-precision arithmetic,Floating point,Computer science,Correctness,Algorithm,Mathematical proof,Proof assistant,Formal proof,Formal verification | Conference |
Volume | ISSN | Citations |
10499 | 0302-9743 | 1 |
PageRank | References | Authors |
0.35 | 9 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sylvie Boldo | 1 | 292 | 26.85 |
| Mioara Joldeş | 2 | 110 | 11.53 |
| Jean-Michel Muller | 3 | 466 | 66.61 |
| Popescu, V. | 4 | 12 | 1.72 |