{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:40:53Z","timestamp":1780994453203,"version":"3.54.1"},"reference-count":81,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2018,12,11]],"date-time":"2018-12-11T00:00:00Z","timestamp":1544486400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF 1535032, 1552975, 1643056, and 1704715"],"award-info":[{"award-number":["CCF 1535032, 1552975, 1643056, and 1704715"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2019,3,31]]},"abstract":"<jats:p>\n            Rigorous estimation of maximum floating-point round-off errors is an important capability central to many formal verification tools. Unfortunately, available techniques for this task often provide very pessimistic overestimates, causing unnecessary verification failure. We have developed a new approach called\n            <jats:italic>Symbolic Taylor Expansions<\/jats:italic>\n            that avoids these problems, and implemented a new tool called FPTaylor embodying this approach. Key to our approach is the use of rigorous global optimization, instead of the more familiar interval arithmetic, affine arithmetic, and\/or SMT solvers. FPTaylor emits per-instance analysis certificates in the form of HOL Light proofs that can be machine checked.\n          <\/jats:p>\n          <jats:p>In this article, we present the basic ideas behind Symbolic Taylor Expansions in detail. We also survey as well as thoroughly evaluate six tool families, namely, Gappa (two tool options studied), Fluctuat, PRECiSA, Real2Float, Rosa, and FPTaylor (two tool options studied) on 24 examples, running on the same machine, and taking care to find the best options for running each of these tools. This study demonstrates that FPTaylor estimates round-off errors within much tighter bounds compared to other tools on a significant number of case studies. We also release FPTaylor along with our benchmarks, thus contributing to future studies and tool development in this area.<\/jats:p>","DOI":"10.1145\/3230733","type":"journal-article","created":{"date-parts":[[2018,12,11]],"date-time":"2018-12-11T13:17:46Z","timestamp":1544534266000},"page":"1-39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":88,"title":["Rigorous Estimation of Floating-Point Round-Off Errors with Symbolic Taylor Expansions"],"prefix":"10.1145","volume":"41","author":[{"given":"Alexey","family":"Solovyev","sequence":"first","affiliation":[{"name":"School of Computing, University of Utah, Salt Lake City, UT, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marek S.","family":"Baranowski","sequence":"additional","affiliation":[{"name":"School of Computing, University of Utah, Salt Lake City, UT, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ian","family":"Briggs","sequence":"additional","affiliation":[{"name":"School of Computing, University of Utah, Salt Lake City, UT, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Charles","family":"Jacobsen","sequence":"additional","affiliation":[{"name":"School of Computing, University of Utah, Salt Lake City, UT, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zvonimir","family":"Rakamari\u0107","sequence":"additional","affiliation":[{"name":"School of Computing, University of Utah, Salt Lake City, UT, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[{"name":"School of Computing, University of Utah, Salt Lake City, UT, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,12,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/3007337.3007352"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the International Conference on Functional Programming (ICFP\u201912)","author":"Alliot Jean-Marc","year":"2012","unstructured":"Jean-Marc Alliot, Nicolas Durand, David Gianazza, and Jean-Baptiste Gotteland. 2012b. Implementing an interval computation library for OCaml on x86\/AMD64 architectures (short paper). In Proceedings of the International Conference on Functional Programming (ICFP\u201912). ACM."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837654"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429133"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_18"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9255-4"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02614-0_10"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-014-9317-x"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2011.40"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Angelo Brillout Daniel Kroening and Thomas Wahl. 2009. Mixed abstractions for floating-point arithmetic. In Formal Methods in Computer-Aided Design (FMCAD\u201909). 69--76.","DOI":"10.1109\/FMCAD.2009.5351141"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89330-1_2"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009846"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2555243.2555265"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_2_1_15_1","unstructured":"Coq 2016. The Coq Proof Assistant. http:\/\/coq.inria.fr."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-016-0435-0"},{"key":"e_1_2_1_19_1","first-page":"458","article-title":"CR-LIBM: A correctly rounded elementary function library. Advanced Signal Processing Algorithms, Architectures, and Implementations XIII","volume":"5205","author":"Daramy Catherine","year":"2003","unstructured":"Catherine Daramy, David Defour, Florent de Dinechin, and Jean-Michel Muller. 2003. CR-LIBM: A correctly rounded elementary function library. Advanced Signal Processing Algorithms, Architectures, and Implementations XIII, SPIE 5205 (2003), 458--464.","journal-title":"SPIE"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048094"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535874"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3014426"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1644001.1644003"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04570-7_6"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1236463.1236468"},{"key":"e_1_2_1_27_1","volume-title":"Retrieved","year":"2017","unstructured":"Frama-C 2017. Frama-C Software Analyzers. Retrieved October 13, 2017 from http:\/\/frama-c.com\/index.html."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"e_1_2_1_29_1","first-page":"713","article-title":"Miller analyzer for Matlab: A Matlab package for automatic roundoff analysis","volume":"31","author":"G\u00e1ti Attila","year":"2012","unstructured":"Attila G\u00e1ti. 2012. Miller analyzer for Matlab: A Matlab package for automatic roundoff analysis. Comput. Inf. 31, 4 (2012), 713--726.","journal-title":"Comput. Inf."},{"key":"e_1_2_1_30_1","volume-title":"Retrieved","author":"Gelpia","year":"2017","unstructured":"Gelpia 2017. Gelpia: A Global Optimizer for Real Functions. Retrieved October 13, 2017 from https:\/\/github.com\/soarlab\/gelpia."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2642940"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/103162.103163"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38088-4_31"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2493882"},{"key":"e_1_2_1_35_1","volume-title":"Retrieved","author":"Goualard Fr\u00e9d\u00e9ric","year":"2017","unstructured":"Fr\u00e9d\u00e9ric Goualard. 2017. GAOL (Not Just Another Interval Library). Retrieved October 13, 2017 from http:\/\/frederic.goualard.net\/#research-software."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946284.1946301"},{"key":"e_1_2_1_37_1","unstructured":"Leopold Haller Alberto Griggio Martin Brain and Daniel Kroening. 2012. Deciding floating-point logic with systematic abstraction. In Formal Methods in Computer-Aided Design (FMCAD\u201912). 131--140."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/646186.683239"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/11757283_8"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_4"},{"key":"e_1_2_1_41_1","volume-title":"IEEE Standard for floating-point arithmetic","year":"2008","unstructured":"2008. IEEE Standard for floating-point arithmetic. IEEE Std 754-2008 (2008), 1--70."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.10.010"},{"key":"e_1_2_1_43_1","volume-title":"Retrieved","author":"Johnson Steven G.","year":"2017","unstructured":"Steven G. Johnson. 2017. The NLopt Nonlinear-Optimization Package. Retrieved October 13, 2017 from https:\/\/nlopt.readthedocs.io\/en\/latest\/."},{"key":"e_1_2_1_44_1","volume-title":"Retrieved","author":"Kahan William","year":"2006","unstructured":"William Kahan. 2006. How Futile Are Mindless Assessments of Roundoff in Floating-Point Computation? Retrieved October 13, 2017 from https:\/\/people.eecs.berkeley.edu\/&sim;wkahan\/Mindless.pdf."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1080\/10556780802614051"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1080\/10556780902753452"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908107"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/2616606.2616749"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1772954.1772987"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3015465"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8608-2"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480945.1480960"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC.2011.52"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC.2013.33"},{"key":"e_1_2_1_55_1","volume-title":"a Computer Algebra System. Version 5.30.0. Retrieved","year":"2013","unstructured":"Maxima. 2013. Maxima, a Computer Algebra System. Version 5.30.0. Retrieved April 3, 2013 from http:\/\/maxima.sourceforge.net\/."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.09.005"},{"key":"e_1_2_1_57_1","volume-title":"An Introduction to Multivariable Analysis from Vector to Manifold","author":"Mikusinski Piotr","unstructured":"Piotr Mikusinski and Michael Taylor. 2002. An Introduction to Multivariable Analysis from Vector to Manifold. Birkh\u00e4user Boston."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/355637.355639"},{"key":"e_1_2_1_59_1","volume-title":"Interval Analysis","author":"Moore R. E.","unstructured":"R. E. Moore. 1966. Interval Analysis. Prentice-Hall."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/143242.143332"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54108-7_17"},{"key":"e_1_2_1_62_1","volume-title":"Retrieved","author":"NASA.","year":"2017","unstructured":"NASA. 2017. NASA World Wind Java SDK. Retrieved October 13, 2017 from http:\/\/worldwind.arc.nasa.gov\/java\/."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023061927787"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0962492904000194"},{"key":"e_1_2_1_65_1","volume-title":"Retrieved","year":"2017","unstructured":"OpenOpt. 2017. OpenOpt: Universal Numerical Optimization Package. Retrieved October 13, 2017 from http:\/\/openopt.org."},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","unstructured":"Gabriele Paganelli and Wolfgang Ahrendt. 2013. Verifying (in-)stability in floating-point programs by increasing precision using SMT solving. In Symbolic and Numeric Algorithms for Scientific Computing (SYNASC\u201913). 209--216. 10.1109\/SYNASC.2013.35","DOI":"10.1109\/SYNASC.2013.35"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737959"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","unstructured":"Olivier Ponsini Claude Michel and Michel Rueher. 2014. Verifying floating-point programs with constraint programming and abstract interpretation techniques. Autom. Softw. Eng. (2014) 1--27. 10.1007\/s10515-014-0154-2","DOI":"10.1007\/s10515-014-0154-2"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"e_1_2_1_70_1","doi-asserted-by":"crossref","unstructured":"N. Revol K. Makino and M. Berz. 2005. Taylor models and floating-point arithmetic: Proof that arithmetic operations are validated in COSY. J. Logic Algebr.c Program. 64 1 (2005) 135--154.","DOI":"10.1016\/j.jlap.2004.07.008"},{"key":"e_1_2_1_71_1","volume-title":"Informal Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (SMT Workshop\u201910)","author":"R\u00fcmmer Philipp","year":"2010","unstructured":"Philipp R\u00fcmmer and Thomas Wahl. 2010. An SMT-LIB theory of binary floating-point arithmetic. In Informal Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (SMT Workshop\u201910)."},{"key":"e_1_2_1_72_1","volume-title":"Retrieved","author":"Solovyev Alexey","year":"2017","unstructured":"Alexey Solovyev. 2017. TOPLAS FPTaylor Results Table. Retrieved October 10, 2017 from http:\/\/tinyurl.com\/TOPLAS-FPTaylor-Results-Table."},{"key":"e_1_2_1_73_1","series-title":"Lecture Notes in Computer Science","volume-title":"Hales","author":"Solovyev Alexey","year":"2013","unstructured":"Alexey Solovyev and Thomas C. Hales. 2013. Formal verification of nonlinear inequalities with Taylor interval approximations. In NASA Formal Methods (NFM\u201913), Lecture Notes in Computer Science, Vol. 7871. Springer, Berlin, 383--397."},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19249-9_33"},{"key":"e_1_2_1_75_1","first-page":"297","article-title":"An introduction to affine arithmetic","volume":"4","author":"Stolfi Jorge","year":"2003","unstructured":"Jorge Stolfi and Luiz H. de Figueiredo. 2003. An introduction to affine arithmetic. TEMA Trends Appl. Comput. Math. 4, 3 (2003), 297--312.","journal-title":"TEMA Trends Appl. Comput. Math."},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/355719.355721"},{"key":"e_1_2_1_77_1","volume-title":"Floating-point arithmetic may give inaccurate results in Excel. https:\/\/support.microsoft.com\/en-us\/help\/78113\/floating-point-arithmetic-may-give-inaccurate-results-in-excel Last updated","author":"Support Microsoft","year":"2018","unstructured":"Microsoft Support. 2018. Floating-point arithmetic may give inaccurate results in Excel. https:\/\/support.microsoft.com\/en-us\/help\/78113\/floating-point-arithmetic-may-give-inaccurate-results-in-excel Last updated April 17, 2018."},{"key":"e_1_2_1_78_1","volume-title":"Retrieved","author":"Surjanovic Sonja","year":"2017","unstructured":"Sonja Surjanovic and Derek Bingham. 2017. Trid Function. Retrieved October 10, 2017 from http:\/\/www.sfu.ca\/%7Essurjano\/trid.html Tridiagonal Examples."},{"key":"e_1_2_1_79_1","volume-title":"Retrieved","author":"Titolo Laura","year":"2017","unstructured":"Laura Titolo. 2017. Schloss Dagstuhl: Seminar Homepage. Retrieved October 10, 2017 from http:\/\/www.dagstuhl.de\/en\/program\/calendar\/semhp\/?semnr&equals;17352."},{"key":"e_1_2_1_80_1","volume-title":"Retrieved","author":"Weisstein Eric","year":"2017","unstructured":"Eric Weisstein. 2017a. Chebyschev Polynomial of the First Kind\u2014From Wolfram MathWorld. Retrieved October 10, 2017 from http:\/\/mathworld.wolfram.com\/ChebyshevPolynomialoftheFirstKind.html."},{"key":"e_1_2_1_81_1","volume-title":"Retrieved","author":"Weisstein Eric","year":"2017","unstructured":"Eric Weisstein. 2017b. Legendre Polynomial\u2014From Wolfram MathWorld. Retrieved October 13, 2017 from http:\/\/mathworld.wolfram.com\/LegendrePolynomial.html."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3230733","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3230733","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3230733","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:57:30Z","timestamp":1750208250000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3230733"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12,11]]},"references-count":81,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,3,31]]}},"alternative-id":["10.1145\/3230733"],"URL":"https:\/\/doi.org\/10.1145\/3230733","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,12,11]]},"assertion":[{"value":"2017-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-12-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}