{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T02:46:18Z","timestamp":1783392378400,"version":"3.54.6"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:p>\n            This paper tackles the important, difficult problem of detecting program inputs that trigger large floating-point errors in numerical code. It introduces a novel, principled\n            <jats:italic>dynamic analysis<\/jats:italic>\n            that leverages the mathematically rigorously analyzed\n            <jats:italic>condition numbers<\/jats:italic>\n            for atomic numerical operations, which we call\n            <jats:italic>atomic conditions<\/jats:italic>\n            , to effectively guide the search for large floating-point errors. Compared with existing approaches, our work based on atomic conditions has several distinctive benefits: (1) it does not rely on high-precision implementations to act as approximate oracles, which are difficult to obtain in general and computationally costly; and (2) atomic conditions provide accurate, modular search guidance. These benefits in combination lead to a highly effective approach that detects more significant errors in real-world code (e.g., widely-used numerical library functions) and achieves several orders of speedups over the state-of-the-art, thus making error analysis significantly more practical. We expect the methodology and principles behind our approach to benefit other floating-point program analysis tasks such as debugging, repair and synthesis. To facilitate the reproduction of our work, we have made our implementation, evaluation data and results publicly available on GitHub at &lt;a&gt;https:\/\/github.com\/FP-Analysis\/atomic-condition&lt;\/a&gt;.\n          <\/jats:p>","DOI":"10.1145\/3371128","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":36,"title":["Detecting floating-point errors via atomic conditions"],"prefix":"10.1145","volume":"4","author":[{"given":"Daming","family":"Zou","sequence":"first","affiliation":[{"name":"Peking University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Muhan","family":"Zeng","sequence":"additional","affiliation":[{"name":"Peking University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yingfei","family":"Xiong","sequence":"additional","affiliation":[{"name":"Peking University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhoulai","family":"Fu","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lu","family":"Zhang","sequence":"additional","affiliation":[{"name":"Peking University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhendong","family":"Su","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1887\/0750306645"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/645511.657075"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509526"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429133"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254118"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2555243.2555265"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236057"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1236463.1236468"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814317"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/103162.103163"},{"key":"e_1_2_2_11_1","volume-title":"VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings (Lecture Notes in Computer Science), Ranjit Jhala and David A. Schmidt (Eds.)","volume":"6538","author":"Goubault Eric","year":"2011","unstructured":"Eric Goubault and Sylvie Putot . 2011 . Static Analysis of Finite Precision Computations. In Verification, Model Checking, and Abstract Interpretation - 12th International Conference , VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings (Lecture Notes in Computer Science), Ranjit Jhala and David A. Schmidt (Eds.) , Vol. 6538 . Springer, 232\u2013247. Eric Goubault and Sylvie Putot. 2011. Static Analysis of Finite Precision Computations. In Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings (Lecture Notes in Computer Science), Ranjit Jhala and David A. Schmidt (Eds.), Vol. 6538. Springer, 232\u2013247."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2009.31"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/502102.502106"},{"key":"e_1_2_2_14_1","doi-asserted-by":"crossref","unstructured":"Nicholas J. Higham. 2002. Accuracy and stability of numerical algorithms (2. ed.). SIAM.  Nicholas J. Higham. 2002. Accuracy and stability of numerical algorithms (2. ed.). SIAM.","DOI":"10.1137\/1.9780898718027"},{"key":"e_1_2_2_15_1","volume-title":"FMCAD 2017","author":"Izycheva Anastasiia","year":"2017","unstructured":"Anastasiia Izycheva and Eva Darulova . 2017 . On sound relative error bounds for floating-point arithmetic. In 2017 Formal Methods in Computer Aided Design , FMCAD 2017 , Vienna, Austria , October 2-6, 2017, Daryl Stewart and Georg Weissenbacher (Eds.). IEEE, 15\u201322. Anastasiia Izycheva and Eva Darulova. 2017. On sound relative error bounds for floating-point arithmetic. In 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017, Daryl Stewart and Georg Weissenbacher (Eds.). IEEE, 15\u201322."},{"key":"e_1_2_2_16_1","unstructured":"Fredrik Johansson et al. 2018. mpmath: a Python library for arbitrary-precision floating-point arithmetic (version 1.1.0). http:\/\/mpmath.org\/.  Fredrik Johansson et al. 2018. mpmath: a Python library for arbitrary-precision floating-point arithmetic (version 1.1.0). http:\/\/mpmath.org\/."},{"key":"e_1_2_2_17_1","volume-title":"Calculus: an intuitive and physical approach","author":"Kline Morris","unstructured":"Morris Kline . 1998. Calculus: an intuitive and physical approach . Courier Corporation . Morris Kline. 1998. Calculus: an intuitive and physical approach. Courier Corporation."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1137\/0701008"},{"key":"e_1_2_2_19_1","volume-title":"2nd IEEE \/ ACM International Symposium on Code Generation and Optimization (CGO 2004)","author":"Lattner Chris","year":"2004","unstructured":"Chris Lattner and Vikram S. Adve . 2004. LLVM: A Compilation Framework for Lifelong Program Analysis &amp; Transformation . In 2nd IEEE \/ ACM International Symposium on Code Generation and Optimization (CGO 2004) , 20-24 March 2004 , San Jose, CA, USA. 75\u201388. Chris Lattner and Vikram S. Adve. 2004. LLVM: A Compilation Framework for Lifelong Program Analysis &amp; Transformation. In 2nd IEEE \/ ACM International Symposium on Code Generation and Optimization (CGO 2004), 20-24 March 2004, San Jose, CA, USA. 75\u201388."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908107"},{"key":"e_1_2_2_21_1","unstructured":"Jacques-Louis Lions Lennart Luebeck Jean-Luc Fauquembergue Gilles Kahn Wolfgang Kubbat Stefan Levedag Leonardo Mazzini Didier Merle and Colin O\u2019Halloran. 1996. Ariane 5 flight 501 failure report by the inquiry board.  Jacques-Louis Lions Lennart Luebeck Jean-Luc Fauquembergue Gilles Kahn Wolfgang Kubbat Stefan Levedag Leonardo Mazzini Didier Merle and Colin O\u2019Halloran. 1996. Ariane 5 flight 501 failure report by the inquiry board."},{"key":"e_1_2_2_22_1","unstructured":"Sandra Loosemore Richard M Stallman Rolandand McGrath Andrew Oram and Ulrich Drepper. 2019. The GNU C Library Reference Manual. (2019). https:\/\/www.gnu.org\/software\/libc\/manual\/html_node\/Errors- in- Math- Functions.html  Sandra Loosemore Richard M Stallman Rolandand McGrath Andrew Oram and Ulrich Drepper. 2019. The GNU C Library Reference Manual. (2019). https:\/\/www.gnu.org\/software\/libc\/manual\/html_node\/Errors- in- Math- Functions.html"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250746"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737959"},{"key":"e_1_2_2_25_1","volume-title":"Exploring Quadruple Precision Floating Point Numbers in GCC and ICC. https:\/\/www.nsc.liu.se\/~pla\/ blog\/2013\/10\/17\/quadruple- precision\/ . [Online","author":"Larsson Peter","year":"2019","unstructured":"Peter Larsson . 2013. Exploring Quadruple Precision Floating Point Numbers in GCC and ICC. https:\/\/www.nsc.liu.se\/~pla\/ blog\/2013\/10\/17\/quadruple- precision\/ . [Online ; accessed 24- June - 2019 ]. Peter Larsson. 2013. Exploring Quadruple Precision Floating Point Numbers in GCC and ICC. https:\/\/www.nsc.liu.se\/~pla\/ blog\/2013\/10\/17\/quadruple- precision\/ . [Online; accessed 24-June-2019]."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00107"},{"key":"e_1_2_2_27_1","volume-title":"Ever had problems rounding off figures. This stock exchange has. The Wall Street Journal","author":"Quinn Kevin","year":"1983","unstructured":"Kevin Quinn . 1983. Ever had problems rounding off figures. This stock exchange has. The Wall Street Journal ( 1983 ), 37. Kevin Quinn. 1983. Ever had problems rounding off figures. This stock exchange has. The Wall Street Journal (1983), 37."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192411"},{"key":"e_1_2_2_29_1","unstructured":"Richard A Silverman etal 1972. Special functions and their applications. Courier Corporation.  Richard A Silverman et al. 1972. Special functions and their applications. Courier Corporation."},{"key":"e_1_2_2_30_1","first-page":"11","article-title":"Roundoff error and the Patriot missile","volume":"25","author":"Skeel Robert","year":"1992","unstructured":"Robert Skeel . 1992 . Roundoff error and the Patriot missile . SIAM News 25 , 4 (1992), 11 . Robert Skeel. 1992. Roundoff error and the Patriot missile. SIAM News 25, 4 (1992), 11.","journal-title":"SIAM News"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230733"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950355"},{"key":"e_1_2_2_33_1","volume-title":"Rounding error changes Parliament makeup. The Risks Digest 13, 37","author":"Weber-Wulff Debora","year":"1992","unstructured":"Debora Weber-Wulff . 1992. Rounding error changes Parliament makeup. The Risks Digest 13, 37 ( 1992 ). Debora Weber-Wulff. 1992. Rounding error changes Parliament makeup. The Risks Digest 13, 37 (1992)."},{"key":"e_1_2_2_34_1","volume-title":"Proceedings of the 3rd International Conference on Genetic Algorithms","author":"Whitley L. Darrell","year":"1989","unstructured":"L. Darrell Whitley . 1989 . The GENITOR Algorithm and Selection Pressure: Why Rank-Based Allocation of Reproductive Trials is Best . In Proceedings of the 3rd International Conference on Genetic Algorithms , George Mason University, Fairfax, Virginia, USA , June 1989, J. David Schaffer (Ed.). Morgan Kaufmann, 116\u2013123. L. Darrell Whitley. 1989. The GENITOR Algorithm and Selection Pressure: Why Rank-Based Allocation of Reproductive Trials is Best. In Proceedings of the 3rd International Conference on Genetic Algorithms, George Mason University, Fairfax, Virginia, USA, June 1989, J. David Schaffer (Ed.). Morgan Kaufmann, 116\u2013123."},{"key":"e_1_2_2_35_1","volume-title":"Efficient Global Search for Inputs Triggering High Floating-Point Inaccuracies. In 24th Asia-Pacific Software Engineering Conference (APSEC). 11\u201320","author":"Yi Xin","year":"2017","unstructured":"Xin Yi , Liqian Chen , Xiaoguang Mao , and Tao Ji . 2017 . Efficient Global Search for Inputs Triggering High Floating-Point Inaccuracies. In 24th Asia-Pacific Software Engineering Conference (APSEC). 11\u201320 . Xin Yi, Liqian Chen, Xiaoguang Mao, and Tao Ji. 2017. Efficient Global Search for Inputs Triggering High Floating-Point Inaccuracies. In 24th Asia-Pacific Software Engineering Conference (APSEC). 11\u201320."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290369"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.70"},{"key":"e_1_2_2_38_1","unstructured":"Dan Zuras Mike Cowlishaw etal 2008. IEEE Standard for Floating-Point Arithmetic. IEEE Std 754-2008 (Aug 2008) 1\u201370.  Dan Zuras Mike Cowlishaw et al. 2008. IEEE Standard for Floating-Point Arithmetic. IEEE Std 754-2008 (Aug 2008) 1\u201370."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371128","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371128","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371128"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":38,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371128"],"URL":"https:\/\/doi.org\/10.1145\/3371128","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}