Name
Abstract | ||
|---|---|---|
We present a new, open-source formalization of fixed and floating-point numbers for arbitrary radix and precision that is now part of the HOL Light distribution John Harrison. HOL Light: A tutorial introduction. In Formal Methods in Computer-Aided Design, pages 265-269. Springer, 1996. We prove correctness and error bounds for the four different rounding modes, and formalize a subset of the IEEE 754 IEEE standard for floating point arithmetic. IEEE Std. 754-2008, 2008 standard by gluing together a set of fixed-point and floating-point numbers to represent the subnormals and normals. In our floating-point proofs, we treat phases of floating-point numbers as copies of fixed-point numbers of varying precision so that we can reuse fixed-point rounding theorems. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1016/j.entcs.2015.10.010 | Electronic Notes in Theoretical Computer Science |
Keywords | DocType | Volume |
IEEE-754-2008,floating point,fixed point,formalization | Journal | 317 |
Issue | ISSN | Citations |
C | 1571-0661 | 4 |
PageRank | References | Authors |
0.40 | 8 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Charles Jacobsen | 1 | 38 | 1.75 |
| Alexey Solovyev | 2 | 205 | 10.13 |
| Ganesh Gopalakrishnan | 3 | 1619 | 130.11 |