{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,30]],"date-time":"2026-05-30T04:37:10Z","timestamp":1780115830660,"version":"3.54.0"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2022,2,22]],"date-time":"2022-02-22T00:00:00Z","timestamp":1645488000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,2,22]],"date-time":"2022-02-22T00:00:00Z","timestamp":1645488000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Constraints"],"published-print":{"date-parts":[[2022,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Verification of programs using floating-point arithmetic is challenging on several accounts. One of the difficulties of reasoning about such programs is due to the peculiarities of floating-point arithmetic: rounding errors, infinities, non-numeric objects (NaNs), signed zeroes, denormal numbers, different rounding modes, etc. One possibility to reason about floating-point arithmetic is to model a program computation path by means of a set of ternary constraints of the form \"Image missing\"and use constraint propagation techniques to infer new information on the variables\u2019 possible values. In this setting, we define and prove the correctness of algorithms to precisely bound the value of one of the variables <jats:italic>x<\/jats:italic>, <jats:italic>y<\/jats:italic> or <jats:italic>z<\/jats:italic>, starting from the bounds known for the other two. We do this for each of the operations and for each rounding mode defined by the IEEE 754 binary floating-point standard, even in the case the rounding mode in effect is only partially known. This is the first time that such so-called <jats:italic>filtering algorithms<\/jats:italic> are defined and their correctness is formally proved. This is an important slab for paving the way to formal verification of programs that use floating-point arithmetics.<\/jats:p>","DOI":"10.1007\/s10601-021-09322-9","type":"journal-article","created":{"date-parts":[[2022,2,22]],"date-time":"2022-02-22T05:02:42Z","timestamp":1645506162000},"page":"29-69","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Correct approximation of IEEE 754 floating-point arithmetic for program verification"],"prefix":"10.1007","volume":"27","author":[{"given":"Roberto","family":"Bagnara","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Abramo","family":"Bagnara","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fabio","family":"Biselli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7742-9233","authenticated-orcid":false,"given":"Michele","family":"Chiari","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Roberta","family":"Gori","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,2,22]]},"reference":[{"key":"9322_CR1","doi-asserted-by":"publisher","unstructured":"Aharoni, M., Asaf, S., Fournier, L., Koyfman, A., & Nagel, R. (2003). FPGen \u2014 a test generation framework for datapath floating-point verification. In Eighth IEEE international high-level design validation and test workshop. https:\/\/doi.org\/10.1109\/HLDVT.2003.1252469 (pp. 17\u201322). San Francisco: IEEE Computer Society.","DOI":"10.1109\/HLDVT.2003.1252469"},{"key":"9322_CR2","volume-title":"Compilers: principles, techniques, and tools","author":"AV Aho","year":"2006","unstructured":"Aho, A.V., Lam, M.S., Sethi, R., & Ullman, J.D. (2006). Compilers: principles, techniques, and tools, 2nd edn. Boston: Addison-Wesley Longman Publishing Co., Inc.","edition":"2nd edn."},{"key":"9322_CR3","unstructured":"Arm Limited: Arm\u00ae Architecture Reference Manual, Armv8, for A-profile architecture edn. (2021). https:\/\/developer.arm.com\/architectures\/cpu-architecture\/a-profile\/docs. Last accessed on October 27th, 2021."},{"key":"9322_CR4","doi-asserted-by":"publisher","unstructured":"Bagnara, R., Carlier, M., Gori, R., & Gotlieb, A. (2013). Symbolic path-oriented test data generation for floating-point programs. In Proceedings of the 6th IEEE international conference on software testing, verification and validation. https:\/\/doi.org\/10.1109\/ICST.2013.17. Luxembourg City: IEEE Press.","DOI":"10.1109\/ICST.2013.17"},{"issue":"1","key":"9322_CR5","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1287\/ijoc.2015.0663","volume":"28","author":"R Bagnara","year":"2016","unstructured":"Bagnara, R., Carlier, M., Gori, R., & Gotlieb, A. (2016). Exploiting binary floating-point representations for constraint propagation. INFORMS Journal on Computing, 28(1), 31\u201346. https:\/\/doi.org\/10.1287\/ijoc.2015.0663.","journal-title":"INFORMS Journal on Computing"},{"issue":"1","key":"9322_CR6","doi-asserted-by":"publisher","first-page":"9:1","DOI":"10.1145\/3410875","volume":"30","author":"R Bagnara","year":"2021","unstructured":"Bagnara, R., Chiari, M., Gori, R., & Bagnara, A. (2021). A practical approach to verification of floating-point C\/C++ programs with math.h\/cmath functions. ACM Transactions on Software Engineering and Methodology, 30(1), 9:1\u20139:53. https:\/\/doi.org\/10.1145\/3410875.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"9322_CR7","doi-asserted-by":"publisher","unstructured":"Barr, E.T., Vo, T., Le, V., & Su, Z. (2013). Automatic detection of floating-point exceptions. In The 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL \u201913, Rome, Italy - January 23 - 25, 2013. https:\/\/doi.org\/10.1145\/2429069.2429133 (pp. 549\u2013560).","DOI":"10.1145\/2429069.2429133"},{"key":"9322_CR8","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., & Tinelli, C. (2011). CVC4. In Computer aided verification, proceedings of the 23rd international conference (CAV 2011), Lecture notes in computer science. https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14, (Vol. 6806 pp. 171\u2013177). Snowbird: Springer.","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"9322_CR9","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., & Tinelli, C. (2018). Satisfiability modulo theories. In E.M. Clarke, T.A. Henzinger, H. Veith, & R. Bloem (Eds.) Handbook of model checking. https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11 (pp. 305\u2013343). Springer.","DOI":"10.1007\/978-3-319-10575-8_11"},{"issue":"2","key":"9322_CR10","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1002\/stvr.333","volume":"16","author":"B Botella","year":"2006","unstructured":"Botella, B., Gotlieb, A., & Michel, C. (2006). Symbolic execution of floating-point computations. Software Testing, Verification and Reliability, 16(2), 97\u2013121. https:\/\/doi.org\/10.1002\/stvr.333.","journal-title":"Software Testing, Verification and Reliability"},{"issue":"2","key":"9322_CR11","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10703-013-0203-7","volume":"45","author":"M Brain","year":"2014","unstructured":"Brain, M., D\u2019Silva, V., Griggio, A., Haller, L., & Kroening, D. (2014). Deciding floating-point logic with abstract conflict driven clause learning. Formal Methods in System Design, 45(2), 213\u2013245. https:\/\/doi.org\/10.1007\/s10703-013-0203-7.","journal-title":"Formal Methods in System Design"},{"key":"9322_CR12","doi-asserted-by":"publisher","unstructured":"Brain, M., Schanda, F., & Sun, Y. (2019). Building better bit-blasting for floating-point problems. In Tools and algorithms for the construction and analysis of systems, proceedings of the 25th international conference (TACAS 2019), Part I, lecture notes in computer science. https:\/\/doi.org\/10.1007\/978-3-030-17462-0_5, (Vol. 11427 pp. 79\u201398). Springer.","DOI":"10.1007\/978-3-030-17462-0_5"},{"key":"9322_CR13","doi-asserted-by":"publisher","unstructured":"Brain, M., Tinelli, C., & R\u00fcmmer, P. (2015). T-wahl: An automatable formal semantics for IEEE-754 floating-point arithmetic. In 22nd IEEE symposium on computer arithmetic (ARITH 2015). https:\/\/doi.org\/10.1109\/ARITH.2015.26 (pp. 160\u2013167). Lyon: IEEE.","DOI":"10.1109\/ARITH.2015.26"},{"key":"9322_CR14","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., & Sebastiani, R. (2013). The mathSAT5 SMT solver. In Tools and algorithms for the construction and analysis of systems, proceedings of the 19th international conference (TACAS 2013), lecture notes in computer science. https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7, (Vol. 7795 pp. 93\u2013107). Springer.","DOI":"10.1007\/978-3-642-36742-7_7"},{"issue":"1","key":"9322_CR15","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/0164-1212(85)90004-4","volume":"5","author":"LA Clarke","year":"1985","unstructured":"Clarke, L.A., & Richardson, D.J. (1985). Applications of symbolic evaluation. Journal of Systems and Software, 5(1), 15\u201335. https:\/\/doi.org\/10.1016\/0164-1212(85)90004-4.","journal-title":"Journal of Systems and Software"},{"key":"9322_CR16","doi-asserted-by":"publisher","unstructured":"Cousot, P., & Cousot, R. (1977). Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the fourth annual ACM symposium on principles of programming languages. https:\/\/doi.org\/10.1145\/512950.512973 (pp. 238\u2013252). Los Angeles: ACM Press.","DOI":"10.1145\/512950.512973"},{"issue":"3","key":"9322_CR17","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/s100920200003","volume":"39","author":"A Cuyt","year":"2002","unstructured":"Cuyt, A., Kuterna, P., Verdonk, B., & Verschaeren, D. (2002). Underflow revisited. CALCOLO, 39(3), 169\u2013179. https:\/\/doi.org\/10.1007\/s100920200003.","journal-title":"CALCOLO"},{"key":"9322_CR18","doi-asserted-by":"publisher","unstructured":"de Moura, L.M., & Bj\u00f8rner, N. (2008). Z3: an efficient SMT solver. In Tools and algorithms for the construction and analysis of systems, proceedings of the 14th international conference (TACAS 2008), lecture notes in computer science. https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24, (Vol. 4963 pp. 337\u2013340). Springer.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9322_CR19","doi-asserted-by":"publisher","unstructured":"Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., & V\u00e9drine, F. (2009). Towards an industrial use of FLUCTUAT on safety-critical avionics software. In Formal methods for industrial critical systems, proceedings of the 14th international workshop (FMICS 2009), lecture notes in computer science. https:\/\/doi.org\/10.1007\/978-3-642-04570-7_6, (Vol. 5825 pp. 53\u201369). Eindhoven: Springer.","DOI":"10.1007\/978-3-642-04570-7_6"},{"key":"9322_CR20","unstructured":"Fiedler, G. (2021). Floating point determinism. Gaffer on games blog, February 24, 2019. https:\/\/gafferongames.com\/post\/floating_point_determinism\/ (2010) Last accessed on October 28th."},{"issue":"3","key":"9322_CR21","doi-asserted-by":"publisher","first-page":"957","DOI":"10.1007\/s11075-019-00711-z","volume":"83","author":"D Gallois-Wong","year":"2020","unstructured":"Gallois-Wong, D., Boldo, S., & Cuoq, P. (2020). Optimal inverse projection of floating-point addition. Numerical Algorithms, 83(3), 957\u2013986. https:\/\/doi.org\/10.1007\/s11075-019-00711-z.","journal-title":"Numerical Algorithms"},{"key":"9322_CR22","doi-asserted-by":"publisher","unstructured":"Gotlieb, A., Botella, B., & Rueher, M. (1998). Automatic test data generation using constraint solving techniques. In Proceedings of the 1998 ACM SIGSOFT international symposium on software testing and analysis, ISSTA \u201998. https:\/\/doi.org\/10.1145\/271771.271790 (pp. 53\u201362). New York: ACM.","DOI":"10.1145\/271771.271790"},{"key":"9322_CR23","doi-asserted-by":"publisher","unstructured":"Gotlieb, A., Botella, B., & Rueher, M. (2000). A CLP framework for computing structural test data. In Computational logic \u2014 CL 2000: first international conference london, UK, July 24\u201328, 2000 Proceedings. https:\/\/doi.org\/10.1007\/3-540-44957-4_27(pp. 399\u2013413). Springer.","DOI":"10.1007\/3-540-44957-4_27"},{"key":"9322_CR24","unstructured":"The Institute of Electrical and Electronics Engineers, Inc.: IEEE Standard for Floating-Point Arithmetic, IEEE Std 754-2008 (revision of IEEE Std 754-1985) edn. (2008). Available at http:\/\/ieeexplore.ieee.org\/servlet\/opac?punumber=4610933."},{"key":"9322_CR25","unstructured":"Intel Corporation. Intel\u00ae 64 and IA-32 Architectures Software Developer Manuals, 325462-075us edn. (2021). https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/articles\/technical\/intel-sdm.html. Last accessed on October 27th, 2021."},{"issue":"7","key":"9322_CR26","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C. (1976). Symbolic execution and program testing. Communications of the ACM, 19(7), 385\u2013394. https:\/\/doi.org\/10.1145\/360248.360252.","journal-title":"Communications of the ACM"},{"key":"9322_CR27","doi-asserted-by":"publisher","unstructured":"Kornerup, P., Lefevre, V., Louvet, N., & Muller, J.M. (2009). On the computation of correctly-rounded sums. In Proceedings of the 19th IEEE symposium on computer arithmetic (ARITH 2009). https:\/\/doi.org\/10.1109\/ARITH.2009.16 (pp. 155\u2013160). Portland.","DOI":"10.1109\/ARITH.2009.16"},{"key":"9322_CR28","unstructured":"Marre, B., Bobot, F., & Chihani, Z. (2017). Real behavior of floating point numbers. In Proceedings of the 15th international workshop on satisfiability modulo theories, CEUR workshop proceedings, (Vol. 1889 pp. 50\u201362)."},{"key":"9322_CR29","doi-asserted-by":"publisher","unstructured":"Marre, B., & Michel, C. (2010). Improving the floating point addition and subtraction constraints. In D. Cohen (Ed.) Proceedings of the 16th international conference on principles and practice of constraint programming (CP 2010), lecture notes in computer science. https:\/\/doi.org\/10.1007\/978-3-642-15396-9_30, (Vol. 6308 pp. 360\u2013367). St. Andrews: Springer.","DOI":"10.1007\/978-3-642-15396-9_30"},{"key":"9322_CR30","unstructured":"Michel, C. (2002). Exact projection functions for floating point number constraints. In Proceedings of the 7th international symposium on artificial intelligence and mathematics. Fort Lauderdale."},{"key":"9322_CR31","doi-asserted-by":"publisher","unstructured":"Michel, C., Rueher, M., & Lebbah, Y. (2001). Solving constraints over floating-point numbers. In Principles and practice of constraint programming - CP 2001, 7th international conference, CP 2001, paphos, cyprus, november 26 - december 1, 2001, proceedings. https:\/\/doi.org\/10.1007\/3-540-45578-7_36 (pp. 524\u2013538).","DOI":"10.1007\/3-540-45578-7_36"},{"key":"9322_CR32","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A. (2004). Relational abstract domains for the detection of floating-point run-time errors. In Programming languages and systems, proceedings of the 13th european symposium on programming (ESOP 2004), lecture notes in computer science. https:\/\/doi.org\/10.1007\/978-3-540-24725-8_2, (Vol. 2986 pp. 3\u201317). Barcelona: Springer.","DOI":"10.1007\/978-3-540-24725-8_2"},{"issue":"3","key":"9322_CR33","doi-asserted-by":"publisher","first-page":"12:1","DOI":"10.1145\/1353445.1353446","volume":"30","author":"D Monniaux","year":"2008","unstructured":"Monniaux, D. (2008). The pitfalls of verifying floating-point computations. ACM Transactions on Programming Languages and Systems, 30(3), 12:1\u201312:41. https:\/\/doi.org\/10.1145\/1353445.1353446.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"9322_CR34","doi-asserted-by":"publisher","unstructured":"M\u00fcller, S.M., & Paul, W.J. (2000). Computer architecture - complexity and correctness springer. https:\/\/doi.org\/10.1007\/978-3-662-04267-0.","DOI":"10.1007\/978-3-662-04267-0"},{"key":"9322_CR35","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/j.cam.2012.09.024","volume":"242","author":"SM Rump","year":"2013","unstructured":"Rump, S.M. (2013). Accurate solution of dense linear systems, Part II: Algorithms using directed rounding. Journal of Computational and Applied Mathematics, 242, 185\u2013212. https:\/\/doi.org\/10.1016\/j.cam.2012.09.024.","journal-title":"Journal of Computational and Applied Mathematics"},{"issue":"2","key":"9322_CR36","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/j.cam.2005.07.038","volume":"199","author":"SM Rump","year":"2007","unstructured":"Rump, S.M., & Ogita, T. (2007). Super-fast validated solution of linear systems. Journal of Computational and Applied Mathematics, 199(2), 199\u2013206. Special Issue on Scientific Computing, Computer Arithmetic, and Validated Numerics (SCAN 2004).","journal-title":"Journal of Computational and Applied Mathematics"},{"key":"9322_CR37","unstructured":"Watte, J. (2021). Floating point determinism. Gamedev.net Forum, June 30, 2008. https:\/\/www.gamedev.net\/forums\/topic\/499435-floating-point-determinism\/ (2008) Last accessed on October 28th."},{"key":"9322_CR38","doi-asserted-by":"publisher","unstructured":"Wu, X., Li, L., & Zhang, J. (2017). Symbolic execution with value-range analysis for floating-point exception detection. In 24th asia-pacific software engineering conference, APSEC 2017, Nanjing, China, December 4\u20138, 2017. https:\/\/doi.org\/10.1109\/APSEC.2017.6 (pp. 1\u201310).","DOI":"10.1109\/APSEC.2017.6"}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-021-09322-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10601-021-09322-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-021-09322-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T06:09:49Z","timestamp":1654063789000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10601-021-09322-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,2,22]]},"references-count":38,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2022,4]]}},"alternative-id":["9322"],"URL":"https:\/\/doi.org\/10.1007\/s10601-021-09322-9","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"value":"1383-7133","type":"print"},{"value":"1572-9354","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,2,22]]},"assertion":[{"value":"7 November 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 February 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}