{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:12:20Z","timestamp":1784837540339,"version":"3.55.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>Floating-point arithmetic is natively supported in hardware and the preferred choice when implementing numerical software in scientific or engineering applications. However, such programs are notoriously hard to analyze due to round-off errors and the frequent use of elementary functions such as log, arctan, or sqrt.<\/jats:p>\n          <jats:p>In this work, we present the Two Variables per Inequality Floating-Point (TVPI-FP) domain, a numerical and constraint-based abstract domain designed for the analysis of floating-point programs. TVPI-FP supports all features of real-world floating-point programs including conditional branches, loops, and elementary functions and it is efficient asymptotically and in practice. Thus it overcomes limitations of prior tools that often are restricted to straight-line programs or require the use of expensive solvers. The key idea is the consistent use of interval arithmetic in inequalities and an associated redesign of all operators. Our extensive experiments show that TVPI-FP is often orders of magnitudes faster than more expressive tools at competitive, or better precision while also providing broader support for realistic programs with loops and conditionals.<\/jats:p>","DOI":"10.1145\/3656395","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"442-466","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Floating-Point TVPI Abstract Domain"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3261-0642","authenticated-orcid":false,"given":"Joao","family":"Rivera","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3529-8973","authenticated-orcid":false,"given":"Franz","family":"Franchetti","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8834-8551","authenticated-orcid":false,"given":"Markus","family":"P\u00fcschel","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"2008. IEEE Standard for Floating-Point Arithmetic. IEEE Std 754\u20132008 (2008) 1-70."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Florian Benz Andreas Hildebrandt and Sebastian Hack. 2012. A Dynamic Program Analysis to Find Floating-Point Accuracy Problems. In Proceedings Conference on Programming Language Design and Implementation (PLDI). 453\u2013462 https:\/\/doi.org\/10.1145\/2254064.2254118 10.1145\/2254064.2254118","DOI":"10.1145\/2254064.2254118"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.softx.2022.101238"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","unstructured":"Liqian Chen Antoine Min\u00e9 and Patrick Cousot. 2008. A Sound Floating-Point Polyhedra Abstract Domain. In Asian Symposium on Programming Languages and Systems (APLAS). 3\u201318. https:\/\/doi.org\/10.1007\/978-3-540-89330-1_2 10.1007\/978-3-540-89330-1_2","DOI":"10.1007\/978-3-540-89330-1_2"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Liqian Chen Antoine Min\u00e9 Ji Wang and Patrick Cousot. 2009. Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships. In Static Analysis Symposium (SAS). 309\u2013325. https:\/\/doi.org\/10.1007\/978-3-642-03237-0_21 10.1007\/978-3-642-03237-0_21","DOI":"10.1007\/978-3-642-03237-0_21"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/2692916.2555265"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","unstructured":"Patrick Cousot and R Cousot. 1976. Static determination of dynamic properties of programs. In Proceedings International Symposium on Programing. 106\u2013130. https:\/\/doi.org\/10.1145\/390019.808314 10.1145\/390019.808314","DOI":"10.1145\/390019.808314"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","unstructured":"Patrick Cousot Radhia Cousot Jer\u00f4me Feret Laurent Mauborgne Antoine Min\u00e9 David Monniaux and Xavier Rival. 2005. The ASTRE\u00c9 Analyzer. In Programming Languages and Systems Mooly Sagiv (Ed.). 21\u201330. https\/\/doi.org\/10.1007\/978-3-540-31987-0_3 10.1007\/978-3-540-31987-0_3","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"Patrick Cousot and Nicolas Halbwachs. 1978. Automatic Discovery of Linear Restraints among Variables of a Program. In Proceedings Symposium on Principles of Programming Languages (POPL). 84\u201396. https:\/\/doi.org\/10.1145\/512760.512770 10.1145\/512760.512770","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","unstructured":"Nasrine Damouche Matthieu Martel Pavel Panchekha Jason Qiu Alex Sanchez-Stern and Zachary Tatlock. 2016. Toward a Standard Benchmark Format and Suite for Floating-Point Analysis. (2016). https:\/\/doi.org\/10.1007\/978-3-319-54292-8_6 10.1007\/978-3-319-54292-8_6","DOI":"10.1007\/978-3-319-54292-8_6"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","unstructured":"Catherine Daramy-Loirat David Defour Florent de Dinechin Matthieu Gallet and Nicolas Gast. 2006. CR-LIBM A library of correctly rounded elementary functions in double-precision. In Research Report. Laboratoire de l\u2019Informatique du Parall\u00e9lisme. http:\/\/dx.doi.org\/10.1117\/12.505591 10.1117\/12.505591","DOI":"10.1117\/12.505591"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"Eva Darulova Anastasiia Izycheva Fariha Nasir Fabian Ritter Heiko Becker and Robert Bastian. 2018. Daisy Framework for Analysis and Optimization of Numerical Programs (Tool Paper). In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 270\u2013287. https:\/\/doi.org\/10.1007\/978-3-319-89960-2_15 10.1007\/978-3-319-89960-2_15","DOI":"10.1007\/978-3-319-89960-2_15"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"Eva Darulova and Viktor Kuncak. 2011. Trustworthy Numerical Computation in Scala. In Proceedings ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA). 325\u2013344. https:\/\/doi.org\/10.1145\/2048066.204809410.1145\/2048066.2048094","DOI":"10.1145\/2048066.2048094"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3014426"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Arnab Das Ian Briggs Ganesh Gopalakrishnan Sriram Krishnamoorthy and Pavel Panchekha. 2020. Scalable yet Rigorous Floating-Point Error Analysis. In Proceedings International Conference for High Performance Computing Networking Storage and Analysis (SC). 1\u201314. https:\/\/doi.org\/10.1109\/SC41405.2020.00055 10.1109\/SC41405.2020.00055","DOI":"10.1109\/SC41405.2020.00055"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/1644001.1644003"},{"key":"e_1_3_2_19_2","unstructured":"L. H. de Figueiredo and J. Stolf. 1997. Self-Validated Numerical Methods and Applications. IMPA\/CNPq (1997)."},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1023\/B:NUMA.0000049462.70970.b6"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","unstructured":"Oliver Flatt and Pavel Panchekha. 2021. An Interval Arithmetic for Robust Error Estimation arXiv:2107.05784 [math.NA] https:\/\/doi.org\/10.48550\/arXiv.2107.05784 10.48550\/arXiv.2107.05784","DOI":"10.48550\/arXiv.2107.05784"},{"key":"e_1_3_2_22_2","unstructured":"M. Galassi. 2023. GNU Scientific Library Reference Manual. http:\/\/www.gnu.org\/software\/gsl\/ Accessed: 09-10-2023."},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_47"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Eric Goubault and Sylvie Putot. 2011. Static Analysis of Finite Precision Computations. In Verification Model Checking and Abstract Interpretation (VMCAI). 232\u2013247. https:\/\/doi.org\/10.1007\/978-3-031-24950-1 10.1007\/978-3-031-24950-1","DOI":"10.1007\/978-3-031-24950-1"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(72)90045-2"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"A. Gurfinkel T. Kahsai A. Komuravelli and J. A. Navas. 2015. The SeaHorn verification framework. Proc. Computer Aided Verification (CAV) (2015) 343\u2013361. https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20 10.1007\/978-3-319-21690-4_20","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898718027"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"e_1_3_2_29_2","first-page":"114","article-title":"Yalaa: Yet another library for affine arithmetic","volume":"16","author":"Kiel S.","year":"2012","unstructured":"S. Kiel. 2012. Yalaa: Yet another library for affine arithmetic. Reliable Computing 16 (2012), 114\u2013129.","journal-title":"Reliable Computing"},{"key":"e_1_3_2_30_2","doi-asserted-by":"crossref","unstructured":"Olga Kupriianova and Christoph Lauter. 2014. Metalibm: A Mathematical Functions Code Generator. In 4th International Congress on Mathematical Software (ICMS). 713\u2013717.","DOI":"10.1007\/978-3-662-44199-2_106"},{"key":"e_1_3_2_31_2","unstructured":"G. Lalire M. Argoud and B. Jeannet. 2023. Interproc. http:\/\/pop-art.inrialpes.fr\/people\/bjeannet\/bjeannet-forge\/interproc\/ Accessed: 10-06-2023."},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","unstructured":"Vincent Laviron and Francesco Logozzo. 2009. SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities. In Verification Model Checking and Abstract Interpretation Neil D. Jones and Markus M\u00fcller-Olm (Eds.). 229\u2013244. https:\/\/doi.org\/10.1007\/978-3-540-93900-9_20 10.1007\/978-3-540-93900-9_20","DOI":"10.1007\/978-3-540-93900-9_20"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/5.726791"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498664"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","unstructured":"Francesco Logozzo and Manuel F\u00e4hndrich. 2008. Pentagons: A Weakly Relational Abstract Domain for the Efficient Validation of Array Accesses. In Proceedings Symposium on Applied Computing (SAC). 184\u2013188. https:\/\/doi.org\/10.1016\/j.scico.2009.04.004 10.1016\/j.scico.2009.04.004","DOI":"10.1016\/j.scico.2009.04.004"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3015465"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"Antoine Min\u00e9. 2002. A few graph-based relational numerical abstract domains. Proc. Static Analysis Symposium (SAS) 117\u2013132. https:\/\/doi.org\/10.1007\/3-540-45789-5_11 10.1007\/3-540-45789-5_11","DOI":"10.1007\/3-540-45789-5_11"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","unstructured":"Antoine Min\u00e9. 2004. Relational abstract domains for the detection of floating-point run-time errors. Proc. European Symposium on Programming (ESOP) 3\u201317. https:\/\/doi.org\/10.1007\/978-3-540-24725-8_2 10.1007\/978-3-540-24725-8_2","DOI":"10.1007\/978-3-540-24725-8_2"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/WCRE.2001.957836"},{"key":"e_1_3_2_40_2","unstructured":"Ramon E. Moore. 1966. Interval Analysis. Prentice-Hall (1966)"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61576-8_77"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-8176-4705-6"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"Olivier Ponsini Claude Michel and Michel Rueher. 2014. Verifying floating-point programs with constraint programming and abstract interpretation techniques. In Automated Software Engineering. 1\u201327. https:\/\/doi.org\/10.1007\/s10515-014-0154-2 10.1007\/s10515-014-0154-2","DOI":"10.1007\/s10515-014-0154-2"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"F.P. Preparata and M.I. Shamos. 1985. Computational Geometry. https:\/\/doi.org\/10.1007\/978-1-4612-1098-6 10.1007\/978-1-4612-1098-6","DOI":"10.1007\/978-1-4612-1098-6"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","unstructured":"Joao Rivera Franz Franchetti and Markus P\u00fcschel. 2021. An Interval Compiler for Sound Floating-Point Computations. In Proceedings International Symposium on Code Generation and Optimization (CGO). 52\u201364. https:\/\/doi.org\/10.1109\/CGO51591.2021.9370307 10.1109\/CGO51591.2021.9370307","DOI":"10.1109\/CGO51591.2021.9370307"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","unstructured":"Joao Rivera Franz Franchetti and Markus P\u00fcschel. 2022. A Compiler for Sound Floating-Point Computations using Affine Arithmetic. In 2022 IEEE\/ACM International Symposium on Code Generation and Optimization (CGO). 66\u201378 https:\/\/doi.org\/10.1109\/CGO53902.2022.9741286 10.1109\/CGO53902.2022.9741286","DOI":"10.1109\/CGO53902.2022.9741286"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-010-9062-8"},{"key":"e_1_3_2_48_2","unstructured":"Gagandeep Singh Timon Gehr Matthew Mirman Markus P\u00fcschel and Martin Vechev. 2018. Fast and Effective Robustness Certification. In Proceedings Proceedings of the 32nd International Conference on Neural Information Processing Systems (NIPS). 10825\u201310836."},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","unstructured":"Gagandeep Singh Timon Gehr Markus P\u00fcschel and Martin Vechev. 2019. An Abstract Domain for Certifying Neural Networks. Proceedings of the ACM on Programming Languages (PACMPL) 3 Article 41 (2019). https:\/\/doi.org\/10.1145\/3290354 10.1145\/3290354","DOI":"10.1145\/3290354"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","unstructured":"Gagandeep Singh Markus P\u00fcschel and Martin Vechev. 2017. Fast Polyhedra Abstract Domain. In Symposium on Principles of Programming Languages (POPL). 46\u201359. https:\/\/doi.org\/10.1145\/3093333.3009885 10.1145\/3093333.3009885","DOI":"10.1145\/3093333.3009885"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3230733"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19249-9_33"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","unstructured":"Laura Titolo Marco A. Feli\u00fa Mariano Moscato and C\u00e9sar A. Mu\u00f1oz. 2018. An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs. In Proceedings Verification Model Checking and Abstract Interpretation (VMCAI). 516\u2013537. https:\/\/doi.org\/10.1007\/978-3-319-73721-8_24 10.1007\/978-3-319-73721-8_24","DOI":"10.1007\/978-3-319-73721-8_24"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_22"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10936-7_19"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656395","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656395","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:39:13Z","timestamp":1751661553000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656395"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":54,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656395"],"URL":"https:\/\/doi.org\/10.1145\/3656395","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}