{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:07:00Z","timestamp":1776305220386,"version":"3.50.1"},"reference-count":70,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2020,12,31]],"date-time":"2020-12-31T00:00:00Z","timestamp":1609372800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2021,1,31]]},"abstract":"<jats:p>\n            Verification of C\/C&lt;bold&gt;++&lt;\/bold&gt; programs has seen considerable progress in several areas, but not for programs that use these languages\u2019 mathematical libraries. The reason is that all libraries in widespread use come with no guarantees about the computed results. This would seem to prevent any attempt at formal verification of programs that use them: without a specification for the functions, no conclusion can be drawn statically about the behavior of the program. We propose an alternative to surrender. We introduce a pragmatic approach that leverages the fact that most &lt;monospace&gt;math.h\/cmath&lt;\/monospace&gt; functions are\n            <jats:italic>almost<\/jats:italic>\n            piecewise monotonic: as we discovered through exhaustive testing, they may have\n            <jats:italic>glitches<\/jats:italic>\n            , often of very small size and in small numbers. We develop interval refinement techniques for such functions based on a modified dichotomic search, which enable verification via symbolic execution based model checking, abstract interpretation, and test data generation. To the best of our knowledge, our refinement algorithms are the first in the literature to be able to handle non-correctly rounded function implementations, enabling verification in the presence of the most common implementations. We experimentally evaluate our approach on real-world code, showing its ability to detect or rule out anomalous behaviors.\n          <\/jats:p>","DOI":"10.1145\/3410875","type":"journal-article","created":{"date-parts":[[2020,12,31]],"date-time":"2020-12-31T18:48:06Z","timestamp":1609440486000},"page":"1-53","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["A Practical Approach to Verification of Floating-Point C\/C++ Programs with math.h\/cmath Functions"],"prefix":"10.1145","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6163-6278","authenticated-orcid":false,"given":"Roberto","family":"Bagnara","sequence":"first","affiliation":[{"name":"University of Parma and BUGSENG srl"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michele","family":"Chiari","sequence":"additional","affiliation":[{"name":"University of Parma, BUGSENG srl, and Politecnico di Milano"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberta","family":"Gori","sequence":"additional","affiliation":[{"name":"University of Pisa"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Abramo","family":"Bagnara","sequence":"additional","affiliation":[{"name":"BUGSENG srl"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,12,31]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Compilers: Principles, Techniques, and Tools","author":"Aho A. V.","year":"2007","unstructured":"A. V. Aho , M. S. Lam , R. Sethi , and J. D. Ullman . 2007 . Compilers: Principles, Techniques, and Tools ( 2 nd ed.). Pearson , London, UK . A. V. Aho, M. S. Lam, R. Sethi, and J. D. Ullman. 2007. Compilers: Principles, Techniques, and Tools (2nd ed.). Pearson, London, UK.","edition":"2"},{"key":"e_1_2_1_2_1","unstructured":"Analog Devices. 2015. C\/C++ Compiler and Library Manual for Blackfin Processors. Revision 1.5. Analog Devices.  Analog Devices. 2015. C\/C++ Compiler and Library Manual for Blackfin Processors. Revision 1.5. Analog Devices."},{"key":"e_1_2_1_3_1","unstructured":"R. Bagnara A. Bagnara F. Biselli M. Chiari and R. Gori. 2019. Correct approximation of IEEE 754 Floating-Point Arithmetic for Program Verification. arXiv:1903.06119[cs.PL]  R. Bagnara A. Bagnara F. Biselli M. Chiari and R. Gori. 2019. Correct approximation of IEEE 754 Floating-Point Arithmetic for Program Verification. arXiv:1903.06119[cs.PL]"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 6th IEEE International Conference on Software Testing, Verification, and Validation. IEEE","author":"Bagnara R.","unstructured":"R. Bagnara , M. Carlier , R. Gori , and A. Gotlieb . 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. IEEE , Los Alamitos, CA, 1--10. R. Bagnara, M. Carlier, R. Gori, and A. Gotlieb. 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. IEEE, Los Alamitos, CA, 1--10."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/3214682.3214685"},{"key":"e_1_2_1_6_1","unstructured":"R. Bagnara M. Chiari R. Gori and A. Bagnara. 2016. A practical approach to interval refinement for math.h\/cmath functions. arXiv:1610.07390[cs.PL]  R. Bagnara M. Chiari R. Gori and A. Bagnara. 2016. A practical approach to interval refinement for math.h\/cmath functions. arXiv:1610.07390[cs.PL]"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201913)","author":"Barr E. T.","unstructured":"E. T. Barr , T. Vo , V. Le , and Z. Su . 2013. Automatic detection of floating-point exceptions . In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201913) . ACM, New York, NY, 549--560. E. T. Barr, T. Vo, V. Le, and Z. Su. 2013. Automatic detection of floating-point exceptions. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201913). ACM, New York, NY, 549--560."},{"key":"e_1_2_1_9_1","volume-title":"Principles and Practice of Constraint Programming. (Lecture Notes in Computer Science","volume":"140","author":"Belaid M. S.","unstructured":"M. S. Belaid , C. Michel , and M. Rueher . 2012. Boosting local consistency algorithms over floating-point numbers . In Principles and Practice of Constraint Programming. (Lecture Notes in Computer Science , Vol. 7514). Springer, 127-- 140 . M. S. Belaid, C. Michel, and M. Rueher. 2012. Boosting local consistency algorithms over floating-point numbers. In Principles and Practice of Constraint Programming. (Lecture Notes in Computer Science, Vol. 7514). Springer, 127--140."},{"key":"e_1_2_1_10_1","volume-title":"Logic Programming: Proceedings of the 1994 International Symposium","author":"Benhamou F.","unstructured":"F. Benhamou , D. McAllester , and P. Van Hentenryck . 1994. CLP(intervals) revisited. In Logic Programming: Proceedings of the 1994 International Symposium . MIT Press Series in Logic Programming, M. Bruynooghe (Ed.). MIT Press , Ithaca, NY, 124--138. F. Benhamou, D. McAllester, and P. Van Hentenryck. 1994. CLP(intervals) revisited. In Logic Programming: Proceedings of the 1994 International Symposium. MIT Press Series in Logic Programming, M. Bruynooghe (Ed.). MIT Press, Ithaca, NY, 124--138."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(96)00142-2"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 5th IEEE International Conference on Software Testing, Verification, and Validation. IEEE","author":"Borges M.","unstructured":"M. Borges , M. d\u2019 Amorim , S. Anand , D. Bushnell , and C. S. Pasareanu . 2012. Symbolic execution with interval solving and meta-heuristic search . In Proceedings of the 5th IEEE International Conference on Software Testing, Verification, and Validation. IEEE , Los Alamitos, CA, 111--120. M. Borges, M. d\u2019Amorim, S. Anand, D. Bushnell, and C. S. Pasareanu. 2012. Symbolic execution with interval solving and meta-heuristic search. In Proceedings of the 5th IEEE International Conference on Software Testing, Verification, and Validation. IEEE, Los Alamitos, CA, 111--120."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1133626.1133628"},{"key":"e_1_2_1_14_1","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis","author":"Brain Martin","unstructured":"Martin Brain , Vijay D\u2019Silva , Alberto Griggio , Leopold Haller , and Daniel Kroening . 2013. Interpolation-based verification of floating-point programs with abstract CDCL . In Static Analysis . Lecture Notes in Computer Science , Vol. 7935 . Springer , 412\u2013432. DOI:https:\/\/doi.org\/10.1007\/978-3-642-38856-9_22 10.1007\/978-3-642-38856-9_22 Martin Brain, Vijay D\u2019Silva, Alberto Griggio, Leopold Haller, and Daniel Kroening. 2013. Interpolation-based verification of floating-point programs with abstract CDCL. In Static Analysis. Lecture Notes in Computer Science, Vol. 7935. Springer, 412\u2013432. DOI:https:\/\/doi.org\/10.1007\/978-3-642-38856-9_22"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 6th International Conference and Exhibition on Embedded Real Time Software and Systems (ERTS\u201912)","author":"Burdy L.","unstructured":"L. Burdy , J.-L. Dufour , and T. Lecomte . 2012. The B method takes up floating-point numbers . In Proceedings of the 6th International Conference and Exhibition on Embedded Real Time Software and Systems (ERTS\u201912) . Article 5C.2, 7 pages. L. Burdy, J.-L. Dufour, and T. Lecomte. 2012. The B method takes up floating-point numbers. In Proceedings of the 6th International Conference and Exhibition on Embedded Real Time Software and Systems (ERTS\u201912). Article 5C.2, 7 pages."},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201908)","author":"Cadar C.","unstructured":"C. Cadar , D. Dunbar , and D. R. Engler . 2008. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs . In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201908) . 209--224. C. Cadar, D. Dunbar, and D. R. Engler. 2008. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201908). 209--224."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0164-1212(85)90004-4"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the 8th European Software Engineering Conference. ACM","author":"Coen-Porisini A.","unstructured":"A. Coen-Porisini , G. Denaro , C. Ghezzi , and M. Pezz\u00e8 . 2001. Using symbolic execution for verifying safety-critical systems . In Proceedings of the 8th European Software Engineering Conference. ACM , New York, NY, 142--151. A. Coen-Porisini, G. Denaro, C. Ghezzi, and M. Pezz\u00e8. 2001. Using symbolic execution for verifying safety-critical systems. In Proceedings of the 8th European Software Engineering Conference. ACM, New York, NY, 142--151."},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the 2nd International Symposium on Programming. 106--130","author":"Cousot P.","year":"1976","unstructured":"P. Cousot and R. Cousot . 1976. Static determination of dynamic properties of programs . In Proceedings of the 2nd International Symposium on Programming. 106--130 . http:\/\/www.di.ens.fr\/ cousot\/publications.www\/CousotCousot-ISOP-76-Dunod-p106--130- 1976 .pdf. P. Cousot and R. Cousot. 1976. Static determination of dynamic properties of programs. In Proceedings of the 2nd International Symposium on Programming. 106--130. http:\/\/www.di.ens.fr\/ cousot\/publications.www\/CousotCousot-ISOP-76-Dunod-p106--130-1976.pdf."},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 4th Annual ACM Symposium on Principles of Programming Languages. ACM","author":"Cousot P.","unstructured":"P. Cousot and R. Cousot . 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints . In Proceedings of the 4th Annual ACM Symposium on Principles of Programming Languages. ACM , New York, NY, 238--252. P. Cousot and R. Cousot. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th Annual ACM Symposium on Principles of Programming Languages. ACM, New York, NY, 238--252."},{"key":"e_1_2_1_21_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science","volume":"10805","author":"Darulova E.","unstructured":"E. Darulova , A. Izycheva , F. Nasir , F. Ritter , H. Becker , and R. Bastian . 2018. Daisy\u2014Framework for analysis and optimization of numerical programs . In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science , Vol. 10805 . Springer, 270--287. E. Darulova, A. Izycheva, F. Nasir, F. Ritter, H. Becker, and R. Bastian. 2018. Daisy\u2014Framework for analysis and optimization of numerical programs. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, Vol. 10805. Springer, 270--287."},{"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.1016\/0004-3702(87)90091-9"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the 18th IEEE International Symposium on Software Reliability (ISSRE\u201907)","author":"Denmat T.","unstructured":"T. Denmat , A. Gotlieb , and M. Ducass\u00e9 . 2007. Improving constraint-based testing with dynamic linear relaxations . In Proceedings of the 18th IEEE International Symposium on Software Reliability (ISSRE\u201907) . IEEE, Los Alamitos, CA, 181--190. T. Denmat, A. Gotlieb, and M. Ducass\u00e9. 2007. Improving constraint-based testing with dynamic linear relaxations. In Proceedings of the 18th IEEE International Symposium on Software Reliability (ISSRE\u201907). IEEE, Los Alamitos, CA, 181--190."},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE\u201917)","author":"Franco A. Di","unstructured":"A. Di Franco , H. Guo , and Cindy C . Rubio-Gonz\u00e1lez. 2017. A comprehensive study of real-world numerical bug characteristics . In Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE\u201917) . IEEE, Los Alamitos, CA, 509--519. A. Di Franco, H. Guo, and Cindy C. Rubio-Gonz\u00e1lez. 2017. A comprehensive study of real-world numerical bug characteristics. In Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE\u201917). IEEE, Los Alamitos, CA, 509--519."},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201917)","author":"Fu Z.","unstructured":"Z. Fu and Z. Su . 2017. Achieving high coverage for floating-point code via unconstrained programming . In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201917) . ACM, New York, NY, 306--319. Z. Fu and Z. Su. 2017. Achieving high coverage for floating-point code via unconstrained programming. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201917). ACM, New York, NY, 306--319."},{"key":"e_1_2_1_28_1","volume-title":"FR Family SOFTUNE C\/C++ Compiler Manual for V6","author":"Semiconductor Fujitsu","unstructured":"Fujitsu Semiconductor . 2013. FR Family SOFTUNE C\/C++ Compiler Manual for V6 ( 8 th ed.). Fujitsu Semiconductor . Fujitsu Semiconductor. 2013. FR Family SOFTUNE C\/C++ Compiler Manual for V6 (8th ed.). Fujitsu Semiconductor.","edition":"8"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI\u201905)","author":"Godefroid P.","unstructured":"P. Godefroid , N. Klarlund , and K. Sen . 2005. DART: Directed automated random testing . In Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI\u201905) . ACM, New York, NY, 213--223. P. Godefroid, N. Klarlund, and K. Sen. 2005. DART: Directed automated random testing. In Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI\u201905). ACM, New York, NY, 213--223."},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the Network and Distributed System Security Symposium (NDSS\u201908)","author":"Godefroid P.","unstructured":"P. Godefroid , M. Y. Levin , and D. A. Molnar . 2008. Automated whitebox fuzz testing . In Proceedings of the Network and Distributed System Security Symposium (NDSS\u201908) . Article 4.1, 16 pages. P. Godefroid, M. Y. Levin, and D. A. Molnar. 2008. Automated whitebox fuzz testing. In Proceedings of the Network and Distributed System Security Symposium (NDSS\u201908). Article 4.1, 16 pages."},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"P. Godefroid and K. Sen. 2018. Combining model checking and testing. In Handbook of Model Checking E. M. Clarke T. A. Henzinger H. Veith and R. Bloem (Eds.). Springer Cham Switzerland 613--649.  P. Godefroid and K. Sen. 2018. Combining model checking and testing. In Handbook of Model Checking E. M. Clarke T. A. Henzinger H. Veith and R. Bloem (Eds.). Springer Cham Switzerland 613--649.","DOI":"10.1007\/978-3-319-10575-8_19"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the 1998 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA\u201998)","author":"Gotlieb A.","unstructured":"A. Gotlieb , B. Botella , and M. Rueher . 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) . ACM, New York, NY, 53--62. A. Gotlieb, B. Botella, and M. Rueher. 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). ACM, New York, NY, 53--62."},{"key":"e_1_2_1_33_1","volume-title":"Computational Logic.Lecture Notes in Artificial Intelligence","volume":"1861","author":"Gotlieb A.","unstructured":"A. Gotlieb , B. Botella , and M. Rueher . 2000. A CLP framework for computing structural test data . In Computational Logic.Lecture Notes in Artificial Intelligence , Vol. 1861 . Springer, 399--413. A. Gotlieb, B. Botella, and M. Rueher. 2000. A CLP framework for computing structural test data. In Computational Logic.Lecture Notes in Artificial Intelligence, Vol. 1861. Springer, 399--413."},{"key":"e_1_2_1_34_1","volume-title":"Programming Languages and Systems.Lecture Notes in Computer Science","volume":"2305","author":"Goubault E.","unstructured":"E. Goubault , M. Martel , and S. Putot . 2002. Asserting the precision of floating-point computations: A simple abstract interpreter . In Programming Languages and Systems.Lecture Notes in Computer Science , Vol. 2305 . Springer, 209--212. E. Goubault, M. Martel, and S. Putot. 2002. Asserting the precision of floating-point computations: A simple abstract interpreter. In Programming Languages and Systems.Lecture Notes in Computer Science, Vol. 2305. Springer, 209--212."},{"key":"e_1_2_1_35_1","volume-title":"Static Analysis. Lecture Notes in Computer Science","volume":"4134","author":"Goubault E.","unstructured":"E. Goubault and S. Putot . 2006. Static analysis of numerical algorithms . In Static Analysis. Lecture Notes in Computer Science , Vol. 4134 . Springer, 18--34. E. Goubault and S. Putot. 2006. Static analysis of numerical algorithms. In Static Analysis. Lecture Notes in Computer Science, Vol. 4134. Springer, 18--34."},{"key":"e_1_2_1_36_1","volume-title":"MULTI: Building Applications for Embedded Power Architecture. Version","author":"Hills Green","year":"2013","unstructured":"Green Hills . 2013 . MULTI: Building Applications for Embedded Power Architecture. Version 2013.1. Green Hills . Green Hills. 2013. MULTI: Building Applications for Embedded Power Architecture. Version 2013.1. Green Hills."},{"key":"e_1_2_1_37_1","volume-title":"MULTI: Building Applications for Embedded V850 and RH850. Version","author":"Hills Green","year":"2013","unstructured":"Green Hills . 2013 . MULTI: Building Applications for Embedded V850 and RH850. Version 2013.5. Green Hills . Green Hills. 2013. MULTI: Building Applications for Embedded V850 and RH850. Version 2013.5. Green Hills."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008712907154"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_14"},{"key":"e_1_2_1_40_1","volume-title":"IEEE Standard for Floating-Point Arithmetic","author":"IEEE Computer Society","year":"2008","unstructured":"IEEE Computer Society . 2008. IEEE Standard for Floating-Point Arithmetic (IEEE Std 754- 2008 [revision of IEEE Std 754-1985] ed.). IEEE Computer Society . IEEE Computer Society. 2008. IEEE Standard for Floating-Point Arithmetic (IEEE Std 754-2008 [revision of IEEE Std 754-1985] ed.). IEEE Computer Society."},{"key":"e_1_2_1_41_1","volume-title":"Base Specifications, Issue 7","author":"IEEE Computer Society and The Open Group. 2013.","year":"2013","unstructured":"IEEE Computer Society and The Open Group. 2013. Standard for Information Technology\u2014 Portable Operating System Interface (POSIX\u00ae) , Base Specifications, Issue 7 (IEEE Std 1003.1, 2013 [incorporates IEEE Std 1003.1-2008 and IEEE Std 1003.1-2008\/Cor 1-2013] ed.). IEEE Computer Society and The Open Group , New York, NY. IEEE Computer Society and The Open Group. 2013. Standard for Information Technology\u2014 Portable Operating System Interface (POSIX\u00ae), Base Specifications, Issue 7 (IEEE Std 1003.1, 2013 [incorporates IEEE Std 1003.1-2008 and IEEE Std 1003.1-2008\/Cor 1-2013] ed.). IEEE Computer Society and The Open Group, New York, NY."},{"key":"e_1_2_1_42_1","volume-title":"Programming Languages\u2014C","author":"International Organization for Standardization. 2011. ISO\/IEC 9899:2011","unstructured":"International Organization for Standardization. 2011. ISO\/IEC 9899:2011 : Programming Languages\u2014C . International Organization for Standardization , Geneva, Switzerland . International Organization for Standardization. 2011. ISO\/IEC 9899:2011: Programming Languages\u2014C. International Organization for Standardization, Geneva, Switzerland."},{"key":"e_1_2_1_43_1","volume-title":"Programming Languages\u2014C++","author":"International Organization for Standardization. 2014. ISO\/IEC 14882:2014(E)","unstructured":"International Organization for Standardization. 2014. ISO\/IEC 14882:2014(E) : Programming Languages\u2014C++ . International Organization for Standardization , Geneva, Switzerland . International Organization for Standardization. 2014. ISO\/IEC 14882:2014(E): Programming Languages\u2014C++. International Organization for Standardization, Geneva, Switzerland."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.57624"},{"key":"e_1_2_1_46_1","unstructured":"P. Lacan J. N. Monfort L. V. Q. Ribal A. Deutsch and G. Gonthier. 1998. ARIANE 5\u2014The software reliability verification process. In DASIA 98: Data Systems in Aerospace (ESA Special Publication Vol. 422) B. H. Kaldeich-Sch\u00fcrmann (Ed.). European Space Agency Athens Greece 201.  P. Lacan J. N. Monfort L. V. Q. Ribal A. Deutsch and G. Gonthier. 1998. ARIANE 5\u2014The software reliability verification process. In DASIA 98: Data Systems in Aerospace (ESA Special Publication Vol. 422) B. H. Kaldeich-Sch\u00fcrmann (Ed.). European Space Agency Athens Greece 201."},{"key":"e_1_2_1_47_1","volume-title":"Proceedings of the 2nd International Symposium on Search Based Software Engineering (SSBSE\u201910)","author":"Lakhotia K.","unstructured":"K. Lakhotia , M. Harman , and H. Gross . 2010. AUSTIN: A tool for search based software testing for the C language and its evaluation on deployed automotive systems . In Proceedings of the 2nd International Symposium on Search Based Software Engineering (SSBSE\u201910) . IEEE, Los Alamitos, CA, 101--110. K. Lakhotia, M. Harman, and H. Gross. 2010. AUSTIN: A tool for search based software testing for the C language and its evaluation on deployed automotive systems. In Proceedings of the 2nd International Symposium on Search Based Software Engineering (SSBSE\u201910). IEEE, Los Alamitos, CA, 101--110."},{"key":"e_1_2_1_48_1","series-title":"Lecture Notes in Computer Science","volume-title":"Testing Software and Systems","author":"Lakhotia K.","unstructured":"K. Lakhotia , N. Tillmann , M. Harman , and J. De Halleux . 2010. FloPSy: Search-based floating point constraint solving for symbolic execution . In Testing Software and Systems . Lecture Notes in Computer Science , Vol. 6435 . Springer , 142--157. K. Lakhotia, N. Tillmann, M. Harman, and J. De Halleux. 2010. FloPSy: Search-based floating point constraint solving for symbolic execution. In Testing Software and Systems. Lecture Notes in Computer Science, Vol. 6435. Springer, 142--157."},{"key":"e_1_2_1_49_1","volume-title":"Proceedings of the ACM on Programming Languages 2, POPL","author":"Lee W.","year":"2018","unstructured":"W. Lee , R. Sharma , and A. Aiken . 2018. On automatically proving the correctness of math.h implementation . Proceedings of the ACM on Programming Languages 2, POPL ( 2018 ), Article 47, 32 pages. W. Lee, R. Sharma, and A. Aiken. 2018. On automatically proving the correctness of math.h implementation. Proceedings of the ACM on Programming Languages 2, POPL (2018), Article 47, 32 pages."},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE\u201917)","author":"Liew D.","unstructured":"D. Liew , D. Schemmel , C. Cadar , A. F. Donaldson , R. Z\u00e4hl , and K. Wehrle . 2017. Floating-point symbolic execution: A case study in n-version programming . In Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE\u201917) . IEEE, Los Alamitos, CA, 601--612. D. Liew, D. Schemmel, C. Cadar, A. F. Donaldson, R. Z\u00e4hl, and K. Wehrle. 2017. Floating-point symbolic execution: A case study in n-version programming. In Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE\u201917). IEEE, Los Alamitos, CA, 601--612."},{"key":"e_1_2_1_51_1","unstructured":"S. Loosemore R. M. Stallman R. McGrath A. Oram and U. Drepper. 2016. The GNU C Library Reference Manual. (version 2.23 ed.). Free Software Foundation Boston MA.  S. Loosemore R. M. Stallman R. McGrath A. Oram and U. Drepper. 2016. The GNU C Library Reference Manual. (version 2.23 ed.). Free Software Foundation Boston MA."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3015465"},{"key":"e_1_2_1_53_1","volume-title":"Proceedings of the 7th International Symposium on Artificial Intelligence and Mathematics. 11","author":"Michel C.","year":"2002","unstructured":"C. Michel . 2002 . Exact projection functions for floating point number constraints . In Proceedings of the 7th International Symposium on Artificial Intelligence and Mathematics. 11 . C. Michel. 2002. Exact projection functions for floating point number constraints. In Proceedings of the 7th International Symposium on Artificial Intelligence and Mathematics. 11."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1976.233818"},{"key":"e_1_2_1_55_1","series-title":"Lecture Notes in Computer Science","volume-title":"Programming Languages and Systems","author":"Min\u00e9 A.","unstructured":"A. Min\u00e9 . 2004. Relational abstract domains for the detection of floating-point run-time errors . In Programming Languages and Systems . Lecture Notes in Computer Science , Vol. 2986 . Springer , 3--17. A. Min\u00e9. 2004. Relational abstract domains for the detection of floating-point run-time errors. In Programming Languages and Systems. Lecture Notes in Computer Science, Vol. 2986. Springer, 3--17."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1353445.1353446"},{"key":"e_1_2_1_57_1","volume-title":"Lecture Notes in Computer Science","volume":"10488","author":"Moscato M.","unstructured":"M. Moscato , L. Titolo , A. Dutle , and C. A. Munoz . 2017. Automatic estimation of verified floating-point round-off errors via static analysis. In Computer Safety, Reliability, and Security . Lecture Notes in Computer Science , Vol. 10488 . Springer, 213--229. M. Moscato, L. Titolo, A. Dutle, and C. A. Munoz. 2017. Automatic estimation of verified floating-point round-off errors via static analysis. In Computer Safety, Reliability, and Security. Lecture Notes in Computer Science, Vol. 10488. Springer, 213--229."},{"key":"e_1_2_1_58_1","unstructured":"J.-M. Muller. 2005. On the Definition of . Rapport de recherche 5504. INRIA.  J.-M. Muller. 2005. On the Definition of . Rapport de recherche 5504. INRIA."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4899-7983-4"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.3888\/tmj.16-11"},{"key":"e_1_2_1_62_1","volume-title":"Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC\/FSE-13)","author":"Sen K.","unstructured":"K. Sen , D. Marinov , and G. Agha . 2005. CUTE: A concolic unit testing engine for C . In Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC\/FSE-13) . ACM, New York, NY, 263--272. K. Sen, D. Marinov, and G. Agha. 2005. CUTE: A concolic unit testing engine for C. In Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC\/FSE-13). ACM, New York, NY, 263--272."},{"key":"e_1_2_1_63_1","article-title":"Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions","volume":"41","author":"Solovyev A.","year":"2018","unstructured":"A. Solovyev , M. S. Baranowski , I. Briggs , C. Jacobsen , Z. Rakamari\u0107 , and G. Gopalakrishnan . 2018 . Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions . ACM Transactions on Programming Languages and Systems 41 , 1 (2018), Article 2, 39 pages. A. Solovyev, M. S. Baranowski, I. Briggs, C. Jacobsen, Z. Rakamari\u0107, and G. Gopalakrishnan. 2018. Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions. ACM Transactions on Programming Languages and Systems 41, 1 (2018), Article 2, 39 pages.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"e_1_2_1_64_1","volume-title":"Proceedings of the 23rd Annual Network and Distributed System Security Symposium (NDSS\u201916)","author":"Stephens N.","unstructured":"N. Stephens , J. Grosen , C. Salls , A. Dutcher , R. Wang , J. Corbetta , Y. Shoshitaishvili , C. Kruegel , and G. Vigna . 2016. Driller: Augmenting fuzzing through selective symbolic execution . In Proceedings of the 23rd Annual Network and Distributed System Security Symposium (NDSS\u201916) . 1--16. N. Stephens, J. Grosen, C. Salls, A. Dutcher, R. Wang, J. Corbetta, Y. Shoshitaishvili, C. Kruegel, and G. Vigna. 2016. Driller: Augmenting fuzzing through selective symbolic execution. In Proceedings of the 23rd Annual Network and Distributed System Security Symposium (NDSS\u201916). 1--16."},{"key":"e_1_2_1_65_1","unstructured":"Texas Instruments. 2018. ARM Optimizing C\/C++ Compiler v18.1.0.LTS User\u2019s Guide. Literature Number: SPNU151R. Texas Instruments.  Texas Instruments. 2018. ARM Optimizing C\/C++ Compiler v18.1.0.LTS User\u2019s Guide. Literature Number: SPNU151R. Texas Instruments."},{"key":"e_1_2_1_66_1","first-page":"1","article-title":"Design, implementation, and evaluation of the constraint language cc(FD)","volume":"37","author":"Hentenryck P. Van","year":"1998","unstructured":"P. Van Hentenryck , V. Saraswat , and Y. Deville . 1998 . Design, implementation, and evaluation of the constraint language cc(FD) . Journal of Logic Programming 37 , 1 \u2013 3 (1998), 139--164. P. Van Hentenryck, V. Saraswat, and Y. Deville. 1998. Design, implementation, and evaluation of the constraint language cc(FD). Journal of Logic Programming 37, 1\u20133 (1998), 139--164.","journal-title":"Journal of Logic Programming"},{"key":"e_1_2_1_67_1","volume-title":"Proceedings of the 24th Asia-Pacific Software Engineering Conference (APSEC\u201917)","author":"Wu X.","unstructured":"X. Wu , L. Li , and J. Zhang . 2017. Symbolic execution with value-range analysis for floating-point exception detection . In Proceedings of the 24th Asia-Pacific Software Engineering Conference (APSEC\u201917) . IEEE, Los Alamitos, CA, 1--10. X. Wu, L. Li, and J. Zhang. 2017. Symbolic execution with value-range analysis for floating-point exception detection. In Proceedings of the 24th Asia-Pacific Software Engineering Conference (APSEC\u201917). IEEE, Los Alamitos, CA, 1--10."},{"key":"e_1_2_1_68_1","volume-title":"Proceedings of the 23rd Asia-Pacific Software Engineering Conference (APSEC\u201916)","author":"Wu X.","unstructured":"X. Wu , Z. Xu , D. Yan , T. Wu , J. Yan , and J. Zhang . 2016. The floating-point extension of symbolic execution engine for bug detection . In Proceedings of the 23rd Asia-Pacific Software Engineering Conference (APSEC\u201916) . IEEE, Los Alamitos, CA, 265--272. X. Wu, Z. Xu, D. Yan, T. Wu, J. Yan, and J. Zhang. 2016. The floating-point extension of symbolic execution engine for bug detection. In Proceedings of the 23rd Asia-Pacific Software Engineering Conference (APSEC\u201916). IEEE, Los Alamitos, CA, 265--272."},{"key":"e_1_2_1_69_1","doi-asserted-by":"crossref","unstructured":"A. Yazdanbakhsh D. Mahajan H. Esmaeilzadeh and P. Lotfi-Kamran. 2017. AxBench: A multiplatform benchmark suite for approximate computing. IEEE Design 8 Test 34 2 (2017) 60--68.  A. Yazdanbakhsh D. Mahajan H. Esmaeilzadeh and P. Lotfi-Kamran. 2017. AxBench: A multiplatform benchmark suite for approximate computing. IEEE Design 8 Test 34 2 (2017) 60--68.","DOI":"10.1109\/MDAT.2016.2630270"},{"key":"e_1_2_1_70_1","first-page":"18","article-title":"Proving a computer system secure","volume":"6","author":"Young W. D.","year":"1985","unstructured":"W. D. Young , W. E. Boebert , and R. Y. Kain . 1985 . Proving a computer system secure . Scientific Honeyweller 6 , 2 (1985), 18 -- 27 . W. D. Young, W. E. Boebert, and R. Y. Kain. 1985. Proving a computer system secure. Scientific Honeyweller 6, 2 (1985), 18--27.","journal-title":"Scientific Honeyweller"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/267580.267590"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3410875","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3410875","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:55Z","timestamp":1750195915000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3410875"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,12,31]]},"references-count":70,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,1,31]]}},"alternative-id":["10.1145\/3410875"],"URL":"https:\/\/doi.org\/10.1145\/3410875","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,12,31]]},"assertion":[{"value":"2019-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-12-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}