{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T16:53:24Z","timestamp":1791478404691,"version":"4.3.4"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2017,3,10]],"date-time":"2017-03-10T00:00:00Z","timestamp":1489104000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"European Research Council (ERC) project \u201cImplicit Programming\u201d"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2017,6,30]]},"abstract":"<jats:p>Numerical software, common in scientific computing or embedded systems, inevitably uses a finite-precision approximation of the real arithmetic in which most algorithms are designed. In many applications, the roundoff errors introduced by finite-precision arithmetic are not the only source of inaccuracy, and measurement and other input errors further increase the uncertainty of the computed results. Adequate tools are needed to help users select suitable data types and evaluate the provided accuracy, especially for safety-critical applications.<\/jats:p>\n          <jats:p>We present a source-to-source compiler called Rosa that takes as input a real-valued program with error specifications and synthesizes code over an appropriate floating-point or fixed-point data type. The main challenge of such a compiler is a fully automated, sound, and yet accurate-enough numerical error estimation. We introduce a unified technique for bounding roundoff errors from floating-point and fixed-point arithmetic of various precisions. The technique can handle nonlinear arithmetic, determine closed-form symbolic invariants for unbounded loops, and quantify the effects of discontinuities on numerical errors. We evaluate Rosa on a number of benchmarks from scientific computing and embedded systems and, comparing it to the state of the art in automated error estimation, show that it presents an interesting tradeoff between accuracy and performance.<\/jats:p>","DOI":"10.1145\/3014426","type":"journal-article","created":{"date-parts":[[2017,3,13]],"date-time":"2017-03-13T12:25:15Z","timestamp":1489407915000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":81,"title":["Towards a Compiler for Reals"],"prefix":"10.1145","volume":"39","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6848-3163","authenticated-orcid":false,"given":"Eva","family":"Darulova","sequence":"first","affiliation":[{"name":"Ecole Polytechnique Federale de Lausanne"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[{"name":"Ecole Polytechnique Federale de Lausanne, Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,3,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","unstructured":"Adolfo Anta Rupak Majumdar Indranil Saha and Paulo Tabuada. 2010. Automatic verification of control system implementations. In EMSOFT. 10.1145\/1879021.1879024","DOI":"10.1145\/1879021.1879024"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","unstructured":"Ali Ayad and Claude March\u00e9. 2010. Multi-prover verification of floating-point programs. In IJCAR. 10.1007\/978-3-642-14203-1_11","DOI":"10.1007\/978-3-642-14203-1_11"},{"key":"e_1_2_1_3_1","unstructured":"David H. Bailey Yozo Hida Xiaoye S. Li and Brandon Thompson. 2013. C++\/Fortran-90 double-double and quad-double package. Retrieved from http:\/\/crd-legacy.lbl.gov\/&sim;dhbailey\/mpdist\/."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Florian Benz Andreas Hildebrandt and Sebastian Hack. 2012. A dynamic program analysis to find floating-point accuracy problems. In PLDI. 10.1145\/2254064.2254118","DOI":"10.1145\/2254064.2254118"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","unstructured":"Bruno Blanchet Patrick Cousot Radhia Cousot J\u00e9rome Feret Laurent Mauborgne Antoine Min\u00e9 David Monniaux and Xavier Rival. 2003. A static analyzer for large safety-critical software. In PLDI. 10.1145\/781131.781153","DOI":"10.1145\/781131.781153"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-011-0099-9"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Martin Brain Cesare Tinelli Philipp R\u00fcmmer and Thomas Wahl. 2015. An automatable formal semantics for IEEE-754 floating-point arithmetic. In ARITH.","DOI":"10.1109\/ARITH.2015.26"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","unstructured":"Angelo Brillout Daniel Kroening and Thomas Wahl. 2009. Mixed abstractions for floating-point arithmetic. In FMCAD. 10.1109\/FMCAD.2009.5351141","DOI":"10.1109\/FMCAD.2009.5351141"},{"key":"e_1_2_1_9_1","unstructured":"CEA-LIST. 2015. Frama-C Software Analyzers. (2015). Retrieved from http:\/\/frama-c.com\/index.html."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","unstructured":"Swarat Chaudhuri Sumit Gulwani Roberto Lublinerman and Sara Navidpour. 2011. Proving programs robust. In ESEC\/FSE. 10.1145\/2025113.2025131","DOI":"10.1145\/2025113.2025131"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","unstructured":"Liqian Chen Antoine Min\u00e9 and Patrick Cousot. 2008. A sound floating-point polyhedra abstract domain. In APLAS. 10.1007\/978-3-540-89330-1_2","DOI":"10.1007\/978-3-540-89330-1_2"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","unstructured":"Wei-Fan Chiang Ganesh Gopalakrishnan Zvonimir Rakamaric and Alexey Solovyev. 2014. Efficient search for inputs causing high floating-point errors. In PPoPP. 10.1145\/2555243.2555265","DOI":"10.1145\/2555243.2555265"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Eva Darulova and Viktor Kuncak. 2011. Trustworthy numerical computation in scala. In OOPSLA. 10.1145\/2048066.2048094","DOI":"10.1145\/2048066.2048094"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","unstructured":"Eva Darulova and Viktor Kuncak. 2014. Sound compilation of reals. In POPL. 10.1145\/2535838.2535874","DOI":"10.1145\/2535838.2535874"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:NUMA.0000049462.70970.b6"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In TACAS.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0962492906350015"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","unstructured":"J\u00e9r\u00f4me Feret. 2004. Static analysis of digital filters. In ESOP. 10.1007\/978-3-540-24725-8_4","DOI":"10.1007\/978-3-540-24725-8_4"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","unstructured":"J\u00e9r\u00f4me Feret. 2005. The arithmetic-geometric progression abstract domain. In VMCAI. 10.1007\/978-3-540-30579-8_3","DOI":"10.1007\/978-3-540-30579-8_3"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/FCCM.2004.59"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","unstructured":"Ivan Gazeau Dale Miller and Catuscia Palamidessi. 2012. A non-local method for robustness analysis of floating point programs. In QAPL. 10.4204\/EPTCS.85.5","DOI":"10.4204\/EPTCS.85.5"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Khalil Ghorbal Eric Goubault and Sylvie Putot. 2009. The zonotope abstract domain taylor1+. In CAV.","DOI":"10.1007\/978-3-642-02658-4_47"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","unstructured":"Khalil Ghorbal Eric Goubault and Sylvie Putot. 2010. A logical product approach to zonotope intersection. In CAV. 10.1007\/978-3-642-14295-6_22","DOI":"10.1007\/978-3-642-14295-6_22"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/103162.103163"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Eric Goubault and Sylvie Putot. 2011. Static analysis of finite precision computations. In VMCAI. 10.1007\/978-3-642-18275-4_17","DOI":"10.1007\/978-3-642-18275-4_17"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","unstructured":"Eric Goubault and Sylvie Putot. 2013. Robustness analysis of finite precision implementations. In APLAS. 10.1007\/978-3-319-03542-0_4","DOI":"10.1007\/978-3-319-03542-0_4"},{"key":"e_1_2_1_29_1","unstructured":"Leopold Haller Alberto Griggio Martin Brain and Daniel Kroening. 2012. Deciding floating-point logic with systematic abstraction. In FMCAD."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/11757283_8"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","unstructured":"Nicholas J. Higham. 2002. Accuracy and Stability of Numerical Algorithms. Siam. 10.1137\/1.9780898718027","DOI":"10.1137\/1.9780898718027"},{"key":"e_1_2_1_32_1","volume-title":"IEEE standard for floating-point arithmetic","author":"Computer Society IEEE. 2008.","year":"2008","unstructured":"Computer Society IEEE. 2008. IEEE standard for floating-point arithmetic. IEEE Std 754-2008 (2008)."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","unstructured":"Franjo Ivancic Malay K. Ganai Sriram Sankaranarayanan and Aarti Gupta. 2010. Numerical stability analysis of floating-point computations using software model checking. In MEMOCODE. 10.1109\/MEMCOD.2010.5558622","DOI":"10.1109\/MEMCOD.2010.5558622"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the 6th International Workshop on Numerical Software Verification (NSV).","author":"Jha Susmit","unstructured":"Susmit Jha and Sanjit A. Seshia. 2013. Synthesis of optimal fixed-point implementations of numerical software routines. In Proceedings of the 6th International Workshop on Numerical Software Verification (NSV)."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","unstructured":"Dejan Jovanovi\u0107 and Leonardo de Moura. 2012. Solving non-linear arithmetic. In IJCAR. 10.1007\/978-3-642-31365-3_27","DOI":"10.1007\/978-3-642-31365-3_27"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2009.5090829"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2464996.2465018"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","unstructured":"Michael O. Lam Jeffrey K. Hollingsworth and G. W. Stewart. 2013a. Dynamic floating-point cancellation detection. Parallel Comput. 39 3 (2013). 10.1016\/j.parco.2012.08.002","DOI":"10.1016\/j.parco.2012.08.002"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2006.873887"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1772954.1772987"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","unstructured":"Rupak Majumdar Indranil Saha and Zilong Wang. 2010. Systematic testing for control applications. In MEMOCODE. 10.1109\/MEMCOD.2010.5558629","DOI":"10.1109\/MEMCOD.2010.5558629"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2006.888291"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","unstructured":"Matthieu Martel. 2002. Static analysis of the numerical stability of loops. In SAS. 10.1007\/3-540-45789-5_12","DOI":"10.1007\/3-540-45789-5_12"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","unstructured":"Antoine Min\u00e9. 2004. Relational abstract domains for the detection of floating-point run-time errors. In ESOP. 10.1007\/978-3-540-24725-8_2","DOI":"10.1007\/978-3-540-24725-8_2"},{"key":"e_1_2_1_46_1","volume-title":"Interval Analysis","author":"Moore Ramon E.","unstructured":"Ramon E. Moore. 1966. Interval Analysis. Prentice-Hall."},{"key":"e_1_2_1_47_1","doi-asserted-by":"crossref","unstructured":"Gabriele Paganelli and Wolfgang Ahrendt. 2013. Verifying (in-)stability in floating-point programs by increasing precision using SMT solving. In SYNASC.","DOI":"10.1109\/SYNASC.2013.35"},{"key":"e_1_2_1_48_1","volume-title":"James Demmel, William Kahan, Koushik Sen, David H. Bailey, Costin Iancu, and David Hough.","author":"Rubio-Gonz\u00e1lez Cindy","year":"2013","unstructured":"Cindy Rubio-Gonz\u00e1lez, Cuong Nguyen, Hong Diep Nguyen, James Demmel, William Kahan, Koushik Sen, David H. Bailey, Costin Iancu, and David Hough. 2013. Precimonious: Tuning assistant for floating-point precision. In SC."},{"key":"e_1_2_1_49_1","volume-title":"Numerical \u2018health check","author":"Scott N. Stan","year":"2007","unstructured":"N. Stan Scott, Fabienne J\u00e9z\u00e9quel, Christophe Denis, and Jean Marie Chesneaux. 2007. Numerical \u2018health check\u2019 for scientific codes: The CADNA approach. Computer Physics Communications (2007)."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","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. 10.1007\/978-3-319-19249-9_33","DOI":"10.1007\/978-3-319-19249-9_33"},{"key":"e_1_2_1_51_1","doi-asserted-by":"crossref","unstructured":"Enyi Tang Earl Barr Xuandong Li and Zhendong Su. 2010. Perturbing numerical calculations for statistical analysis of floating-point program (in)stability. In ISSTA.","DOI":"10.1145\/1831708.1831724"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-1366-6"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3014426","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3014426","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:23:17Z","timestamp":1750220597000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3014426"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3,10]]},"references-count":49,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,6,30]]}},"alternative-id":["10.1145\/3014426"],"URL":"https:\/\/doi.org\/10.1145\/3014426","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,3,10]]},"assertion":[{"value":"2015-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-03-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}