{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,31]],"date-time":"2025-07-31T00:45:00Z","timestamp":1753922700410,"version":"3.41.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2022,6,30]],"date-time":"2022-06-30T00:00:00Z","timestamp":1656547200000},"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":["Form. Asp. Comput."],"published-print":{"date-parts":[[2022,6,30]]},"abstract":"<jats:p>We present a method for formal verification of transcendental hardware and software algorithms that scales to higher precision without suffering an exponential growth in runtimes. A class of implementations using piecewise polynomial approximation to compute the result is verified using MetiTarski, an automated theorem prover, which verifies a range of inputs for each call. The method was applied to commercial implementations from Cadence Design Systems with significant runtime gains over exhaustive testing methods and was successful in proving that the expected accuracy of one implementation was overly optimistic. Reproducing the verification of a sine implementation in software, previously done using an alternative theorem-proving technique, demonstrates that the MetiTarski approach is a viable competitor. Verification of a 52-bit implementation of the square root function highlights the method\u2019s high-precision capabilities.<\/jats:p>","DOI":"10.1145\/3543670","type":"journal-article","created":{"date-parts":[[2022,6,13]],"date-time":"2022-06-13T12:21:59Z","timestamp":1655122919000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover"],"prefix":"10.1145","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7741-3271","authenticated-orcid":false,"given":"Samuel","family":"Coward","sequence":"first","affiliation":[{"name":"Faculty of Mathematics, University of Cambridge, London, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0288-4279","authenticated-orcid":false,"given":"Lawrence","family":"Paulson","sequence":"additional","affiliation":[{"name":"Computer Laboratory, University of Cambridge, Cambridge, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6488-5440","authenticated-orcid":false,"given":"Theo","family":"Drane","sequence":"additional","affiliation":[{"name":"Cadence Design Systems, Folsom, CA, United States"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1154-1016","authenticated-orcid":false,"given":"Emiliano","family":"Morini","sequence":"additional","affiliation":[{"name":"Cadence Design Systems, Folsom, CA, United States"}]}],"member":"320","published-online":{"date-parts":[[2022,9,19]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/978-3-540-85110-3_18","volume-title":"International Conference on Intelligent Computer Mathematics","author":"Akbarpour Behzad","year":"2008","unstructured":"Behzad Akbarpour and Lawrence C. Paulson. 2008. MetiTarski: An automatic prover for the elementary functions. In International Conference on Intelligent Computer Mathematics. Springer, 217\u2013231."},{"key":"e_1_3_1_3_2","first-page":"1","volume-title":"Hybrid Systems: Computation and Control (LNCS 5469)","author":"Akbarpour Behzad","year":"2009","unstructured":"Behzad Akbarpour and Lawrence C. Paulson. 2009. Applications of MetiTarski in the verification of control and hybrid systems. In Hybrid Systems: Computation and Control (LNCS 5469), Rupak Majumdar and Paulo Tabuada (Eds.). Springer, 1\u201315."},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9149-2"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/275107.275139"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/12.295857"},{"key":"e_1_3_1_7_2","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1109\/ARITH.2007.20","volume-title":"18th IEEE Symposium on Computer Arithmetic","author":"Boldo Sylvie","year":"2007","unstructured":"Sylvie Boldo and Jean-Christophe Filli\u00e2tre. 2007. Formal verification of floating-point programs. In 18th IEEE Symposium on Computer Arithmetic. IEEE, 187\u2013194."},{"key":"e_1_3_1_8_2","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/978-3-642-02614-0_10","volume-title":"International Conference on Intelligent Computer Mathematics","author":"Boldo Sylvie","year":"2009","unstructured":"Sylvie Boldo, Jean-Christophe Filli\u00e2tre, and Guillaume Melquiond. 2009. Combining Coq and Gappa for certifying floating-point programs. In International Conference on Intelligent Computer Mathematics. Springer, 59\u201374."},{"key":"e_1_3_1_9_2","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1109\/ARITH.2011.40","volume-title":"20th IEEE Symposium on Computer Arithmetic (ARITH\u201911)","author":"Boldo Sylvie","year":"2011","unstructured":"Sylvie Boldo and Guillaume Melquiond. 2011. Flocq: A unified library for proving floating-point algorithms in Coq. In 20th IEEE Symposium on Computer Arithmetic (ARITH\u201911). IEEE, 243\u2013252."},{"key":"e_1_3_1_10_2","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1109\/ARITH.2007.17","volume-title":"18th IEEE Symposium on Computer Arithmetic (ARITH\u201907)","author":"Brisebarre Nicolas","year":"2007","unstructured":"Nicolas Brisebarre and Sylvain Chevillard. 2007. Efficient polynomial L-approximations. In 18th IEEE Symposium on Computer Arithmetic (ARITH\u201907). IEEE, 169\u2013176."},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/968708.968710"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2011.43"},{"key":"e_1_3_1_13_2","first-page":"195","volume-title":"19th IEEE Symposium on Computer Arithmetic","author":"Chen D.","year":"2009","unstructured":"D. Chen, Y. Zhang, Y. Choi, M. H. Lee, and S. Ko. 2009. A 32-bit decimal floating-point logarithmic converter. In 19th IEEE Symposium on Computer Arithmetic. IEEE, 195\u2013203."},{"key":"e_1_3_1_14_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1007\/978-3-642-15582-6_5","volume-title":"Mathematical Software (ICMS\u201910)","author":"Chevillard S.","year":"2010","unstructured":"S. Chevillard, M. Jolde\u015f, and C. Lauter. 2010. Sollya: An environment for the development of numerical codes. In Mathematical Software (ICMS\u201910)(Lecture Notes in Computer Science, Vol. 6327), K. Fukuda, J. van der Hoeven, M. Joswig, and N. Takayama (Eds.). Springer, Heidelberg, Germany, 28\u201331."},{"key":"e_1_3_1_15_2","first-page":"95","volume-title":"International Conference on Automated Deduction","author":"Cimatti Alessandro","year":"2017","unstructured":"Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani. 2017. Satisfiability modulo transcendental functions via incremental linearization. In International Conference on Automated Deduction. Springer, 95\u2013113."},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/1096483"},{"issue":"2","key":"e_1_3_1_17_2","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1109\/TC.2008.213","article-title":"Verified real number calculations: A library for interval arithmetic","volume":"58","author":"Daumas Marc","year":"2008","unstructured":"Marc Daumas, David Lester, and C\u00e9sar Munoz. 2008. Verified real number calculations: A library for interval arithmetic. IEEE Trans. Comput. 58, 2 (2008), 226\u2013237.","journal-title":"IEEE Trans. Comput."},{"issue":"1","key":"e_1_3_1_18_2","first-page":"2","article-title":"Certification of bounds on expressions involving rounded operators","volume":"37","author":"Daumas Marc","year":"2010","unstructured":"Marc Daumas and Guillaume Melquiond. 2010. Certification of bounds on expressions involving rounded operators. ACM Transactions on Mathematical Software (TOMS) 37, 1 (2010), 2.","journal-title":"ACM Transactions on Mathematical Software (TOMS)"},{"key":"e_1_3_1_19_2","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-44755-5_13","volume-title":"International Conference on Theorem Proving in Higher Order Logics","author":"Daumas Marc","year":"2001","unstructured":"Marc Daumas, Laurence Rideau, and Laurent Th\u00e9ry. 2001. A generic library for floating-point numbers and its application to exact computing. In International Conference on Theorem Proving in Higher Order Logics. Springer, 169\u2013184."},{"key":"e_1_3_1_20_2","first-page":"216","volume-title":"Application-specific Systems, Architectures and Processors","author":"Dinechin Florent de","year":"2010","unstructured":"Florent de Dinechin, Mioara Joldes, and Bogdan Pasca. 2010. Automatic generation of polynomial-based hardware architectures for function evaluation. In Application-specific Systems, Architectures and Processors. IEEE, 216\u2013222."},{"issue":"2","key":"e_1_3_1_21_2","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1109\/TC.2010.128","article-title":"Certifying the floating-point implementation of an elementary function using Gappa","volume":"60","author":"Dinechin F. de","year":"2011","unstructured":"F. de Dinechin, C. Lauter, and G. Melquiond. 2011. Certifying the floating-point implementation of an elementary function using Gappa. IEEE Trans. Comput. 60, 2 (2011), 242\u2013253.","journal-title":"IEEE Trans. Comput."},{"key":"e_1_3_1_22_2","first-page":"1318","volume-title":"ACM Symposium on Applied Computing","author":"Dinechin Florent De","year":"2006","unstructured":"Florent De Dinechin, Christoph Quirin Lauter, and Guillaume Melquiond. 2006. Assisted verification of elementary functions using Gappa. In ACM Symposium on Applied Computing. ACM, 1318\u20131322."},{"issue":"4","key":"e_1_3_1_23_2","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1109\/MDT.2011.44","article-title":"Designing custom arithmetic data paths with FloPoCo","volume":"28","author":"Dinechin Florent de","year":"2011","unstructured":"Florent de Dinechin and Bogdan Pasca. 2011. Designing custom arithmetic data paths with FloPoCo. IEEE Design & Test of Computers 28, 4 (July 2011), 18\u201327.","journal-title":"IEEE Design & Test of Computers"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_1_25_2","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1109\/FMCAD.2009.5351136","volume-title":"Formal Methods in Computer-Aided Design, 2009 (FMCAD\u201909)","author":"Denman William","year":"2009","unstructured":"William Denman, Behzad Akbarpour, Sofiene Tahar, Mohamed H. Zaki, and Lawrence C. Paulson. 2009. Formal verification of analog designs using MetiTarski. In Formal Methods in Computer-Aided Design, 2009 (FMCAD\u201909). IEEE, 93\u2013100."},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/1236463.1236468"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/12.204796"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/103147.103151"},{"key":"e_1_3_1_29_2","first-page":"208","volume-title":"International Conference on Automated Deduction","author":"Gao Sicun","year":"2013","unstructured":"Sicun Gao, Soonho Kong, and Edmund M. Clarke. 2013. dReal: An SMT solver for nonlinear theories over the reals. In International Conference on Automated Deduction. Springer, 208\u2013214."},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/103162.103163"},{"key":"e_1_3_1_31_2","first-page":"1641","volume-title":"Conference Record of 35th Asilomar Conference on Signals, Systems and Computers (Cat. No. 01CH37256)","volume":"2","author":"Harris David","year":"2001","unstructured":"David Harris. 2001. A powering unit for an OpenGL lighting engine. In Conference Record of 35th Asilomar Conference on Signals, Systems and Computers (Cat. No. 01CH37256), Vol. 2. IEEE, 1641\u20131645."},{"key":"e_1_3_1_32_2","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/BFb0000475","volume-title":"International Conference on Algebraic Methodology and Software Technology","author":"Harrison John","year":"1997","unstructured":"John Harrison. 1997. Floating point verification in HOL Light: The exponential function. In International Conference on Algebraic Methodology and Software Technology. Springer, 246\u2013260."},{"key":"e_1_3_1_33_2","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/3-540-48256-3_9","volume-title":"International Conference on Theorem Proving in Higher Order Logics","author":"Harrison John","year":"1999","unstructured":"John Harrison. 1999. A machine-checked theory of floating point arithmetic. In International Conference on Theorem Proving in Higher Order Logics. Springer, 113\u2013130."},{"key":"e_1_3_1_34_2","first-page":"211","volume-title":"International School on Formal Methods for the Design of Computer, Communication and Software Systems","author":"Harrison John","year":"2006","unstructured":"John Harrison. 2006. Floating-point verification using theorem proving. In International School on Formal Methods for the Design of Computer, Communication and Software Systems. Springer, 211\u2013242."},{"key":"e_1_3_1_35_2","first-page":"187","volume-title":"19th IEEE Symposium on Computer Arithmetic","author":"Harrison J.","year":"2009","unstructured":"J. Harrison. 2009. Decimal transcendentals via binary. In 19th IEEE Symposium on Computer Arithmetic. IEEE, 187\u2013194."},{"key":"e_1_3_1_36_2","volume-title":"Intel Technology Journal","author":"Harrison John","year":"1999","unstructured":"John Harrison, Ted Kubaska, Shane Story, and Ping Tak Peter Tang. 1999. The computation of transcendental functions on the IA-64 architecture. In Intel Technology Journal. Citeseer."},{"key":"e_1_3_1_37_2","unstructured":"Wolfram Research Inc.2021. Mathematica Version 12.1. https:\/\/www.wolfram.com\/mathematica."},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1613-y"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908107"},{"key":"e_1_3_1_40_2","unstructured":"Joe Leslie-Hurd. 2007. Metis Theorem Prover. http:\/\/www.gilith.com\/software\/metis\/."},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/4.482205"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1117\/12.505591"},{"key":"e_1_3_1_43_2","first-page":"348","volume-title":"International Conference on Logic for Programming Artificial Intelligence and Reasoning","author":"Ludwig Michel","year":"2007","unstructured":"Michel Ludwig and Uwe Waldmann. 2007. An extension of the Knuth-Bendix ordering with LPO-like properties. In International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer, 348\u2013362."},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9350-4"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.09.005"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.29007\/b63g"},{"key":"e_1_3_1_47_2","unstructured":"J. Strother Moore Tom Lynch and Matt Kaufmann. 1996. A mechanically checked proof of the correctness of the kernel of the AMD5k86 floating point division algorithm. http:\/\/devil.ece.utexas.edu."},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-8176-4705-6"},{"key":"e_1_3_1_49_2","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1109\/ASAP.2002.1030708","volume-title":"Proceedings of the IEEE International Conference on Application- Specific Systems, Architectures, and Processors","author":"Pineiro J.","year":"2002","unstructured":"J. Pineiro, M. D. Ercegovac, and J. D. Bruguera. 2002. High-radix logarithm with selection by rounding. In Proceedings of the IEEE International Conference on Application- Specific Systems, Architectures, and Processors. IEEE, 101\u2013110."},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2004.53"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2005.52"},{"key":"e_1_3_1_52_2","first-page":"97","volume-title":"Colloquium on Trees in Algebra and Programming","author":"Pratt Vaughan","year":"1995","unstructured":"Vaughan Pratt. 1995. Anatomy of the Pentium bug. In Colloquium on Trees in Algebra and Programming. Springer, 97\u2013107."},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1112\/S1461157000000176"},{"key":"e_1_3_1_54_2","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1109\/ARITH.1993.378099","volume-title":"Proceedings of IEEE 11th Symposium on Computer Arithmetic","author":"Schulte M.","year":"1993","unstructured":"M. Schulte and E. Swartzlander. 1993. Exact rounding of certain elementary functions. In Proceedings of IEEE 11th Symposium on Computer Arithmetic. IEEE, 138\u2013145."},{"issue":"1","key":"e_1_3_1_55_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3230733","article-title":"Rigorous estimation of floating-point round-off errors with symbolic taylor expansions","volume":"41","author":"Solovyev Alexey","year":"2018","unstructured":"Alexey Solovyev, Marek S. Baranowski, Ian Briggs, Charles Jacobsen, Zvonimir Rakamari\u0107, and Ganesh Gopalakrishnan. 2018. Rigorous estimation of floating-point round-off errors with symbolic taylor expansions. ACM Transactions on Programming Languages and Systems (TOPLAS) 41, 1 (2018), 1\u201339.","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"e_1_3_1_56_2","first-page":"4","volume-title":"Proceedings of the 14th IEEE Symposium on Computer Arithmetic","author":"Story Shane","year":"1999","unstructured":"Shane Story and Ping Tak Peter Tang. 1999. New algorithms for improved transcendental functions on IA-64. In Proceedings of the 14th IEEE Symposium on Computer Arithmetic. IEEE, 4\u201311."},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2010.127"},{"key":"e_1_3_1_58_2","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1109\/ARITH.1991.145565","volume-title":"10th IEEE Symposium on Computer Arithmetic","author":"Tang Ping Tak Peter","year":"1991","unstructured":"Ping Tak Peter Tang. 1991. Table-lookup algorithms for elementary functions and their error analysis. In 10th IEEE Symposium on Computer Arithmetic. IEEE, 232\u2013236."},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01386215"},{"key":"e_1_3_1_60_2","doi-asserted-by":"publisher","DOI":"10.1145\/1457838.1457886"},{"key":"e_1_3_1_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/1478786.1478840"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3543670","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3543670","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:48Z","timestamp":1750186848000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3543670"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,30]]},"references-count":60,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,6,30]]}},"alternative-id":["10.1145\/3543670"],"URL":"https:\/\/doi.org\/10.1145\/3543670","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2022,6,30]]},"assertion":[{"value":"2020-11-18","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-05-30","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-09-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}