{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,24]],"date-time":"2025-03-24T08:56:59Z","timestamp":1742806619333,"version":"3.37.3"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"The floating-point representation provides widely-used data types (such as \u201cfloat\u201d and \u201cdouble\u201d) for modern numerical software. Numerical errors are inherent due to floating-point\u2019s approximate nature, and pose an important, well-known challenge. It is nontrivial to fix\/repair numerical code to reduce numerical errors \u2014 it requires eithernumerical expertise<\/jats:italic>(for manual fixing) or high-precisionoracles<\/jats:italic>(for automatic repair); both are difficult requirements. To tackle this challenge, this paper introduces aprincipled dynamic approach<\/jats:italic>that isfully automated<\/jats:italic>andoracle-free<\/jats:italic>for effectively repairing floating-point errors. The key of our approach is the novel notion ofmicro-structure<\/jats:italic>that characterizes structural patterns of floating-point errors. We leverage micro-structures\u2019 statistical information on floating-point errors to effectively guide repair synthesis and validation. Compared with existing state-of-the-art repair approaches, our work is fully automatic and has the distinctive benefit of not relying on the difficult to obtain high-precision oracles. Evaluation results on 36 commonly-used numerical programs show that our approach is highly efficient and effective: (1) it is able to synthesize repairs instantaneously, and (2) versus the original programs, the repaired programs have orders of magnitude smaller floating-point errors, while having faster runtime performance.<\/jats:p>","DOI":"10.1145\/3563322","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"957-985","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Oracle-free repair synthesis for floating-point programs"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9562-6492","authenticated-orcid":false,"given":"Daming","family":"Zou","sequence":"first","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5805-2901","authenticated-orcid":false,"given":"Yuchen","family":"Gu","sequence":"additional","affiliation":[{"name":"Peking University, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3189-2713","authenticated-orcid":false,"given":"Yuanfeng","family":"Shi","sequence":"additional","affiliation":[{"name":"Peking University, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4405-1494","authenticated-orcid":false,"given":"MingZhe","family":"Wang","sequence":"additional","affiliation":[{"name":"Princeton University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8991-747X","authenticated-orcid":false,"given":"Yingfei","family":"Xiong","sequence":"additional","affiliation":[{"name":"Peking University, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2970-1391","authenticated-orcid":false,"given":"Zhendong","family":"Su","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Milton Abramowitz Irene A Stegun and Robert H Romer. 1988. Handbook of mathematical functions with formulas graphs and mathematical tables. Milton Abramowitz Irene A Stegun and Robert H Romer. 1988. Handbook of mathematical functions with formulas graphs and mathematical tables.","DOI":"10.1119\/1.15378"},{"key":"e_1_2_1_2_1","volume-title":"IFIP Congress (1). 68","author":"Babuska Ivo","year":"1968","unstructured":"Ivo Babuska . 1968 . Numerical stability in mathematical analysis .. In IFIP Congress (1). 68 , 11\u201323. Ivo Babuska. 1968. Numerical stability in mathematical analysis.. In IFIP Congress (1). 68, 11\u201323."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509526"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254118"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/362003.362037"},{"key":"e_1_2_1_6_1","unstructured":"Richard L Burden and J Faires. 2010. Numerical analysis (9th). Richard L Burden and J Faires. 2010. Numerical analysis (9th)."},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Fran\u00e7oise Chatelin and Marie-Christine Brunet. 1990. A probabilistic round-off error propagation model. application to the eigenvalue problem. Cox and Hammarling [CH90] 139\u2013160. Fran\u00e7oise Chatelin and Marie-Christine Brunet. 1990. A probabilistic round-off error propagation model. application to the eigenvalue problem. Cox and Hammarling [CH90] 139\u2013160.","DOI":"10.1093\/oso\/9780198535645.003.0009"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2555243.2555265"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386004"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3468585"},{"key":"e_1_2_1_11_1","volume-title":"National Physical Laboratory Mathematical Tables","volume":"5","author":"Clenshaw C.W.","year":"1962","unstructured":"C.W. Clenshaw . 1962 . Chebyshev series for mathematical functions . National Physical Laboratory Mathematical Tables , Vol. 5 .. C.W. Clenshaw. 1962. Chebyshev series for mathematical functions. National Physical Laboratory Mathematical Tables, Vol. 5.."},{"key":"e_1_2_1_12_1","volume-title":"David J Jeffrey, and Donald E Knuth.","author":"Corless Robert M","year":"1996","unstructured":"Robert M Corless , Gaston H Gonnet , David EG Hare , David J Jeffrey, and Donald E Knuth. 1996 . On the LambertW function. Advances in Computational mathematics, 5, 1 (1996), 329\u2013359. Robert M Corless, Gaston H Gonnet, David EG Hare, David J Jeffrey, and Donald E Knuth. 1996. On the LambertW function. Advances in Computational mathematics, 5, 1 (1996), 329\u2013359."},{"key":"e_1_2_1_13_1","volume-title":"Salsa: An Automatic Tool to Improve the Numerical Accuracy of Programs.. In AFM@ NFM. 63\u201376.","author":"Damouche Nasrine","year":"2017","unstructured":"Nasrine Damouche and Matthieu Martel . 2017 . Salsa: An Automatic Tool to Improve the Numerical Accuracy of Programs.. In AFM@ NFM. 63\u201376. Nasrine Damouche and Matthieu Martel. 2017. Salsa: An Automatic Tool to Improve the Numerical Accuracy of Programs.. In AFM@ NFM. 63\u201376."},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Biswa Nath Datta. 2010. Numerical linear algebra and applications. 116 SIAM. Biswa Nath Datta. 2010. Numerical linear algebra and applications. 116 SIAM.","DOI":"10.1137\/1.9780898717655"},{"key":"e_1_2_1_15_1","volume-title":"Hendrik Paul Lopuha\u00e4, and Ludolf Erwin Meester","author":"Dekking Frederik Michel","year":"2005","unstructured":"Frederik Michel Dekking , Cornelis Kraaikamp , Hendrik Paul Lopuha\u00e4, and Ludolf Erwin Meester . 2005 . A Modern Introduction to Probability and Statistics: Understanding why and how. Springer Science & Business Media . Frederik Michel Dekking, Cornelis Kraaikamp, Hendrik Paul Lopuha\u00e4, and Ludolf Erwin Meester. 2005. A Modern Introduction to Probability and Statistics: Understanding why and how. Springer Science & Business Media."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236057"},{"volume-title":"The Gauss-Markov theorem in multivariate analysis","author":"Eaton Morris L","key":"e_1_2_1_17_1","unstructured":"Morris L Eaton . 1983. The Gauss-Markov theorem in multivariate analysis . University of Minnesota . Morris L Eaton. 1983. The Gauss-Markov theorem in multivariate analysis. University of Minnesota."},{"volume-title":"An introduction to numerical methods and analysis","author":"Epperson James F","key":"e_1_2_1_18_1","unstructured":"James F Epperson . 2013. An introduction to numerical methods and analysis . John Wiley & Sons . James F Epperson. 2013. An introduction to numerical methods and analysis. John Wiley & Sons."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1236463.1236468"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814317"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cam.2012.11.021"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Amparo Gil Javier Segura and Nico M Temme. 2007. Numerical methods for special functions. SIAM. Amparo Gil Javier Segura and Nico M Temme. 2007. Numerical methods for special functions. SIAM.","DOI":"10.1137\/1.9780898717822"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380359"},{"volume-title":"Numerical methods for scientists and engineers","author":"Hamming Richard","key":"e_1_2_1_24_1","unstructured":"Richard Hamming . 2012. Numerical methods for scientists and engineers . Courier Corporation . Richard Hamming. 2012. Numerical methods for scientists and engineers. Courier Corporation."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1137\/18M1226312"},{"volume-title":"Introduction to numerical analysis","author":"Hildebrand Francis Begnaud","key":"e_1_2_1_26_1","unstructured":"Francis Begnaud Hildebrand . 1987. Introduction to numerical analysis . Courier Corporation . Francis Begnaud Hildebrand. 1987. Introduction to numerical analysis. Courier Corporation."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/363707.363723"},{"key":"e_1_2_1_28_1","unstructured":"William Kahan. 2004. A logarithm too clever by half. William Kahan. 2004. A logarithm too clever by half."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434310"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454049"},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Jay P Lim and Santosh Nagarakatte. 2021. RLIBM-ALL: A Novel Polynomial Approximation Method to Produce Correctly Rounded Results for Multiple Representations and Rounding Modes. arXiv preprint arXiv:2108.06756. Jay P Lim and Santosh Nagarakatte. 2021. RLIBM-ALL: A Novel Polynomial Approximation Method to Produce Correctly Rounded Results for Multiple Representations and Rounding Modes. arXiv preprint arXiv:2108.06756.","DOI":"10.1145\/3498664"},{"key":"e_1_2_1_32_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."},{"volume-title":"Chebyshev polynomials","author":"Mason John C","key":"e_1_2_1_33_1","unstructured":"John C Mason and David C Handscomb . 2002. Chebyshev polynomials . CRC press . John C Mason and David C Handscomb. 2002. Chebyshev polynomials. CRC press."},{"key":"e_1_2_1_34_1","unstructured":"William Mendenhall Robert J Beaver and Barbara M Beaver. 2012. Introduction to probability and statistics. Cengage Learning. William Mendenhall Robert J Beaver and Barbara M Beaver. 2012. Introduction to probability and statistics. Cengage Learning."},{"key":"e_1_2_1_35_1","unstructured":"Jean-Michel Muller. 2005. On the definition of ulp (x). Ph. D. Dissertation. INRIA LIP. Jean-Michel Muller. 2005. On the definition of ulp (x). Ph. D. Dissertation. INRIA LIP."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02242136"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250746"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0025-5718-1974-0373227-8"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0771-050X(79)90002-0"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737959"},{"key":"e_1_2_1_41_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":"2021","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 : 2021 -01-01] 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: 2021-01-01]"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00107"},{"volume-title":"Principles of mathematical analysis. 3","author":"Rudin Walter","key":"e_1_2_1_43_1","unstructured":"Walter Rudin . 1976. Principles of mathematical analysis. 3 , McGraw-hill New York . Walter Rudin. 1976. Principles of mathematical analysis. 3, McGraw-hill New York."},{"volume-title":"Modern regression methods. 655","author":"Ryan Thomas P","key":"e_1_2_1_44_1","unstructured":"Thomas P Ryan . 2008. Modern regression methods. 655 , John Wiley & Sons . Thomas P Ryan. 2008. Modern regression methods. 655, John Wiley & Sons."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192411"},{"key":"e_1_2_1_46_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_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230733"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01934204"},{"key":"e_1_2_1_49_1","volume-title":"Toyota: Software to blame for Prius brake problems","author":"Valdes-Dapena Peter","year":"2010","unstructured":"Peter Valdes-Dapena and Kyung Lah . 2010 . Toyota: Software to blame for Prius brake problems . http:\/\/edition.cnn.com\/2010\/WORLD\/asiapcf\/02\/04\/japan.prius.complaints\/index.html [Online; Accessed: 2021-01-01] Peter Valdes-Dapena and Kyung Lah. 2010. Toyota: Software to blame for Prius brake problems. http:\/\/edition.cnn.com\/2010\/WORLD\/asiapcf\/02\/04\/japan.prius.complaints\/index.html [Online; Accessed: 2021-01-01]"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3395363.3397380"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950355"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00116"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2017.7"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290369"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.70"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371128"},{"key":"e_1_2_1_57_1","volume-title":"IEEE Standard for Floating-Point Arithmetic","author":"Zuras Dan","year":"2008","unstructured":"Dan Zuras and Mike Cowlishaw . 2008. IEEE Standard for Floating-Point Arithmetic . IEEE Std 754- 2008 , Aug, 1\u201370. Dan Zuras and Mike Cowlishaw. 2008. IEEE Standard for Floating-Point Arithmetic. IEEE Std 754-2008, Aug, 1\u201370."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563322","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,29]],"date-time":"2023-11-29T21:22:08Z","timestamp":1701292928000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563322"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":57,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563322"],"URL":"https:\/\/doi.org\/10.1145\/3563322","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}