Loading...
Journal ArticlesACM Transactions on Programming Languages and Systems (TOPLAS)Year : 2008
The pitfalls of verifying floating-point computations
David Monniaux (1, 2)
David Monniaux
Connectez-vous pour contacter l'auteur
- Function :Correspondent author
- PersonId :9093
- IdHAL :david-monniaux
- ORCID :0000-0001-7671-6126
- IdRef :070681600
Connectez-vous pour contacter l'auteur
Abstract
Current critical systems commonly use a lot of floating-point computations, and thus the testing or static analysis of programs containing floating-point operators has become a priority. However, correctly defining the semantics of common implementations of floating-point is tricky, because semantics may change with many factors beyond source-code level, such as choices made by compilers. We here give concrete examples of problems that can appear and solutions to implement in analysis software.
| Origin | Files produced by the author(s) |
|---|
Loading...
Contact
![](#"https://hal.science/hal-00128124v5/document"><div><i aria-hidden="true"></i><span>Download</span></div></a></div><div><h3> Dates and versions</h3><div><span>hal-00128124 ,</span><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fhal.science%2fhal-00128124v1"> version 1</a></span><span>(30-01-2007)</span></div><div><span>hal-00128124 ,</span><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fhal.science%2fhal-00128124v2"> version 2</a></span><span>(20-04-2007)</span></div><div><span>hal-00128124 ,</span><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fhal.science%2fhal-00128124v3"> version 3</a></span><span>(29-06-2007)</span></div><div><span>hal-00128124 ,</span><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fhal.science%2fhal-00128124v4"> version 4</a></span><span>(25-10-2007)</span></div><div><span>hal-00128124 ,</span><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fhal.science%2fhal-00128124v5"> version 5</a></span><span>(22-05-2008)</span></div><h3> Identifiers</h3><div><ul><li><span> HAL Id :</span><span> hal-00128124 , version 5</span></li><li><span> ARXIV :</span><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2farxiv.org%2fabs%2fcs%2f0701192"> cs/0701192</a></span></li><li><span> DOI :</span><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fdx.doi.org%2f10.1145%2f1353445.1353446"> 10.1145/1353445.1353446</a></span></li></ul></div></div><div><div><h3> Cite</h3><button><span></span></button></div><div> David Monniaux. The pitfalls of verifying floating-point computations.<i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>, 2008, 30 (3), pp.12.<a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fdx.doi.org%2f10.1145%2f1353445.1353446">⟨10.1145/1353445.1353446⟩</a>.<a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fhal.science%2fhal-00128124v5">⟨hal-00128124v5⟩</a></div></div><div><h3> Export</h3><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fhal.science%2fhal-00128124v5%2fbibtex">BibTeX</a></span><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fhal.science%2fhal-00128124v5%2ftei">XML-TEI</a></span><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fhal.science%2fhal-00128124v5%2fdc">Dublin Core</a></span><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fhal.science%2fhal-00128124v5%2fdcterms">DC Terms</a></span><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fhal.science%2fhal-00128124v5%2fendnote">EndNote</a></span><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fhal.science%2fhal-00128124v5%2fdatacite">DataCite</a></span></div><div><h3> Collections</h3><div><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fhal.science%2fENS-PARIS" > ENS-PARIS</a></span><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fhal.science%2fUGA" > UGA</a></span><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fhal.science%2fIMAG" > IMAG</a></span><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fhal.science%2fCNRS" > CNRS</a></span><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fhal.science%2fVERIMAG" > VERIMAG</a></span><span><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fhal.science%2fPSL" > PSL</a></span></div></div><div><div><div><span> 14548</span><span>View</span></div><div><span> 23015</span><span>Download</span></div></div></div><div><h3> Altmetric</h3><div data-badge-details="right" data-badge-type="donut" data-hide-no-mentions="false" data-doi="10.1145/1353445.1353446" ></div></div><div><h3> Share</h3><div ><ul><li><a></a><span></span></li><li><a></a><span></span></li><li><a></a><span></span></li><li><a></a><span></span></li><li><a></a><span></span></li><li><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fwww.addtoany.com%2fshare"></a><span> More</span></li></ul></div></div></section></section></main><footer><div><div><a href="/mt/?noimg=&dark=on&url=https%3a%2f%2fwww.enseignementsup-recherche.gouv.fr%2f" rel="noopener"><img src="/image.pl?url=https%3a%2f%2fhal.science%2fpublic%2fmesr.svg&f=jpg&w=240" alt="Ministère de l){kind=link}
Legal issues
CCSD
[8]ページ先頭
©2009-2025 Movatter.jp