{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:23:12Z","timestamp":1770279792931,"version":"3.49.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1160904, CCF-1409813"],"award-info":[{"award-number":["CCF-1160904, CCF-1409813"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>Industry standard implementations of math.h claim (often without formal proof) tight bounds on floating-point errors. We demonstrate a novel static analysis that proves these bounds and verifies the correctness of these implementations. Our key insight is a reduction of this verification task to a set of mathematical optimization problems that can be solved by off-the-shelf computer algebra systems. We use this analysis to prove the correctness of implementations in Intel's math library automatically. Prior to this work, these implementations could only be verified with significant manual effort.<\/jats:p>","DOI":"10.1145\/3158135","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["On automatically proving the correctness of math.h implementations"],"prefix":"10.1145","volume":"2","author":[{"given":"Wonyeol","family":"Lee","sequence":"first","affiliation":[{"name":"Stanford University, USA"}]},{"given":"Rahul","family":"Sharma","sequence":"additional","affiliation":[{"name":"Microsoft Research, India"}]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[{"name":"Stanford University, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429133"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254118"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1088\/1749-4699\/2\/1\/015001"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2555243.2555265"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1966445.1966475"},{"key":"e_1_2_2_7_1","unstructured":"Catherine Daramy-Loirat David Defour Florent de Dinechin Matthieu Gallet Nicolas Gast and Jean-Michel Muller. 2005. CR-Libm a library of correctly rounded elementary functions in double-precision. Available at http:\/\/lipforge.enslyon.fr\/www\/crlibm . Catherine Daramy-Loirat David Defour Florent de Dinechin Matthieu Gallet Nicolas Gast and Jean-Michel Muller. 2005. CR-Libm a library of correctly rounded elementary functions in double-precision. Available at http:\/\/lipforge.enslyon.fr\/www\/crlibm ."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535874"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1644001.1644003"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2010.128"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01397083"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04570-7_6"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062383"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/103162.103163"},{"key":"e_1_2_2_15_1","unstructured":"Eric Goubault and Sylvie Putot. 2005. Weakly relational domains for floating-point computation analysis. In NSAD. Eric Goubault and Sylvie Putot. 2005. Weakly relational domains for floating-point computation analysis. In NSAD."},{"key":"e_1_2_2_16_1","doi-asserted-by":"crossref","unstructured":"Eric Goubault Sylvie Putot Philippe Baufreton and Jean Gassino. 2007. Static Analysis of the Accuracy in Control Systems: Principles and Experiments. In FMICS. 3\u201320. Eric Goubault Sylvie Putot Philippe Baufreton and Jean Gassino. 2007. Static Analysis of the Accuracy in Control Systems: Principles and Experiments. In FMICS. 3\u201320.","DOI":"10.1007\/978-3-540-79707-4_3"},{"key":"e_1_2_2_17_1","unstructured":"Leopold Haller Alberto Griggio Martin Brain and Daniel Kroening. 2012. Deciding floating-point logic with systematic abstraction. In FMCAD. 131\u2013140. Leopold Haller Alberto Griggio Martin Brain and Daniel Kroening. 2012. Deciding floating-point logic with systematic abstraction. In FMCAD. 131\u2013140."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_9"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008712907154"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_14"},{"key":"e_1_2_2_21_1","unstructured":"William Kahan. 2004. A logarithm too clever by half. Available at http:\/\/http.cs.berkeley.edu\/~wkahan\/LOG10HAF.TXT . William Kahan. 2004. A logarithm too clever by half. Available at http:\/\/http.cs.berkeley.edu\/~wkahan\/LOG10HAF.TXT ."},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Kiran Lakhotia Nikolai Tillmann Mark Harman and Jonathan de Halleux. 2010. FloPSy - Search-Based Floating Point Constraint Solving for Symbolic Execution. In ICTSS. 142\u2013157. Kiran Lakhotia Nikolai Tillmann Mark Harman and Jonathan de Halleux. 2010. FloPSy - Search-Based Floating Point Constraint Solving for Symbolic Execution. In ICTSS. 142\u2013157.","DOI":"10.1007\/978-3-642-16573-3_11"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908107"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.09.005"},{"key":"e_1_2_2_25_1","doi-asserted-by":"crossref","unstructured":"Antoine Min\u00e9. 2012. Abstract Domains for Bit-Level Machine Integer and Floating-point Operations. In ATx\/WInG. 55\u201370. Antoine Min\u00e9. 2012. Abstract Domains for Bit-Level Machine Integer and Floating-point Operations. In ATx\/WInG. 55\u201370.","DOI":"10.29007\/b63g"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_24"},{"key":"e_1_2_2_27_1","unstructured":"Jean-Michel Muller. 2005. On the definition of ulp(x). Available at http:\/\/ljk.imag.fr\/membres\/Carine.Lucas\/TPScilab\/ JMMuller\/ulp- toms.pdf . Jean-Michel Muller. 2005. On the definition of ulp(x). Available at http:\/\/ljk.imag.fr\/membres\/Carine.Lucas\/TPScilab\/ JMMuller\/ulp- toms.pdf ."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_1"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2931021.2931024"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854066"},{"key":"e_1_2_2_31_1","doi-asserted-by":"crossref","unstructured":"Eric Schkufza Rahul Sharma and Alex Aiken. 2014. Stochastic Optimization of Floating-Point Programs using Tunable Precision. In PLDI. 53\u201364. Eric Schkufza Rahul Sharma and Alex Aiken. 2014. Stochastic Optimization of Floating-Point Programs using Tunable Precision. In PLDI. 53\u201364.","DOI":"10.1145\/2666356.2594302"},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Alexey Solovyev Charles Jacobsen Zvonimir Rakamaric and Ganesh Gopalakrishnan. 2015. Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions. In FM. 532\u2013550. Alexey Solovyev Charles Jacobsen Zvonimir Rakamaric and Ganesh Gopalakrishnan. 2015. Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions. In FM. 532\u2013550.","DOI":"10.1007\/978-3-319-19249-9_33"},{"key":"e_1_2_2_33_1","volume-title":"Floating-point computation","author":"Sterbenz Pat H."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158135","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158135","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158135","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,29]],"date-time":"2025-06-29T09:16:24Z","timestamp":1751188584000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158135"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":33,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158135"],"URL":"https:\/\/doi.org\/10.1145\/3158135","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}