{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T12:16:42Z","timestamp":1754396202706,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031666759"},{"type":"electronic","value":"9783031666766"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-66676-6_13","type":"book-chapter","created":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T12:04:18Z","timestamp":1725451458000},"page":"251-270","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["ACL2 Support for\u00a0Floating-Point Computations"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-5667-4888","authenticated-orcid":false,"given":"Matt","family":"Kaufmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9628-1702","authenticated-orcid":false,"given":"J Strother","family":"Moore","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,4]]},"reference":[{"key":"13_CR1","unstructured":"ACL2 User Community: ACL2 community books. https:\/\/github.com\/acl2\/acl2\/tree\/master\/books"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Boyer, R.S., Moore, J.S.: Single-threaded objects in ACL2. In: Krishnamurthi, S., Ramakrishnan, C.R. (eds.) Practical Aspects of Declarative Languages, 4th International Symposium, PADL 2002, Portland, OR, USA, January 19-20, 2002, Proceedings. Lecture Notes in Computer Science, vol.\u00a02257, pp. 9\u201327. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45587-6_3, https:\/\/doi.org\/10.1007\/3-540-45587-6_3","DOI":"10.1007\/3-540-45587-6_3"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Brock, B., Kaufmann, M., Moore, J.S.: ACL2 theorems about commercial microprocessors. In: Srivas, M., Camilleri, A. (eds.) Formal Methods in Computer-Aided Design (FMCAD\u201996), pp. 275\u2013293. Springer-Verlag, LNCS 1166, Heidelberg (November 1996). https:\/\/doi.org\/10.1007\/BFb0031816, http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/bkm96.ps.Z","DOI":"10.1007\/BFb0031816"},{"key":"13_CR4","doi-asserted-by":"publisher","unstructured":"Hunt, Jr., W., Kaufmann, M., Moore, J.S., Slobodova, A.: Industrial hardware and software verification with ACL2. In: Verified Trustworthy Software Systems. vol.\u00a0375. The Royal Society (2017).https:\/\/doi.org\/10.1098\/rsta.2015.0399, (Article Number 20150399)","DOI":"10.1098\/rsta.2015.0399"},{"key":"13_CR5","doi-asserted-by":"publisher","unstructured":"Hunt, Jr., W.A., Ramanathan, V., Moore, J.S.: Vwsim: A circuit simulator. In: Sumners, R., Chau, C. (eds.) Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022. Electronic Proceedings in Theoretical Computer Science, vol.\u00a0359, pp. 61\u201375. Open Publishing Association (2022). https:\/\/doi.org\/10.4204\/EPTCS.359.7","DOI":"10.4204\/EPTCS.359.7"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Kaufmann, M., Manolios, P., J S.\u00a0Moore: Computer-Aided Reasoning: An Approach. Kluwer Academic Press, Boston, MA. (2000). https:\/\/doi.org\/10.1007\/978-1-4615-4449-4","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"13_CR7","unstructured":"Kaufmann, M., Moore, J.S.: The ACL2 home page. In: Department of Computer Sciences, University of Texas at Austin (2024). http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/"},{"key":"13_CR8","unstructured":"Kaufmann, M., J S.\u00a0Moore: ACL2 Documentation for DF. http:\/\/acl2.org\/manual\/index.html?topic=ACL2____DF"},{"key":"13_CR9","unstructured":"Kaufmann, M., J S.\u00a0Moore: ACL2 Documentation for Partial Encapsulation. http:\/\/acl2.org\/manual\/index.html?topic=ACL2____PARTIAL-ENCAPSULATE"},{"key":"13_CR10","unstructured":"Kaufmann, M., J S.\u00a0Moore: ACL2 Documentation for TERM. http:\/\/acl2.org\/manual\/index.html?topic=ACL2____TERM"},{"key":"13_CR11","unstructured":"Kaufmann, M., J S.\u00a0Moore, The ACL2 Community: The Combined ACL2+Books User\u2019s Manual. http:\/\/acl2.org\/manual\/index.html (2021)"},{"key":"13_CR12","unstructured":"LispWorks: Common Lisp Documentation. http:\/\/www.lispworks.com\/documentation\/common-lisp.html"},{"key":"13_CR13","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D., et al. (eds.) Automated Deduction\u2014CADE-11, pp. 748\u2013752. Springer Berlin Heidelberg, Berlin, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"key":"13_CR14","unstructured":"Pitman, K.: The Common Lisp HyperSpec. https:\/\/www.lispworks.com\/documentation\/HyperSpec\/Front\/"},{"key":"13_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-87181-9","volume-title":"Formal Verification of Floating-Point Hardware Design: A Mathematical Approach","author":"David M Russinoff","year":"2022","unstructured":"Russinoff, David M.: Formal Verification of Floating-Point Hardware Design: A Mathematical Approach, 2nd edn. Springer International Publishing, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-87181-9","edition":"2"},{"key":"13_CR16","unstructured":"Standards Committee of the IEEE Computer Society: IEEE standard for binary floating-point arithmetic. Tech. Rep. IEEE Std. 754-1985, IEEE, 345 East 47th Street, New York, NY 10017 (1985)"}],"container-title":["Lecture Notes in Computer Science","The Practice of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66676-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T12:06:45Z","timestamp":1725451605000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66676-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031666759","9783031666766"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66676-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"4 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}}]}}