{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T00:48:57Z","timestamp":1768438137910,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540278825","type":"print"},{"value":"9783540317142","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11526841_35","type":"book-chapter","created":{"date-parts":[[2010,7,18]],"date-time":"2010-07-18T16:51:58Z","timestamp":1279471918000},"page":"529-532","source":"Crossref","is-referenced-by-count":7,"title":["Floating-Point Verification"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"35_CR1","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers\u00a0C-35, 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"35_CR2","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation\u00a098, 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"35_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"35_CR4","first-page":"1","volume":"1998-Q2","author":"M. Cornea-Hasegan","year":"1998","unstructured":"Cornea-Hasegan, M.: Proving the IEEE correctness of iterative floating-point square root, divide and remainder algorithms. Intel Technology Journal\u00a01998-Q2, 1\u201311 (1998), available on the web, http:\/\/developer.intel.com\/technology\/itj\/q21998\/articles\/art_3.htm","journal-title":"Intel Technology Journal"},{"key":"35_CR5","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"35_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"35_CR7","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Theorem Proving with the Real Numbers. Springer-Verlag, Revised version of author\u2019s PhD thesis (1998)","DOI":"10.1007\/978-1-4471-1591-5"},{"key":"35_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-48256-3_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1999","unstructured":"Harrison, J.: A machine-checked theory of floating point arithmetic. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 113\u2013130. Springer, Heidelberg (1999)"},{"key":"35_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-40922-X_14","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"2000","unstructured":"Harrison, J.: Formal verification of floating point trigonometric functions. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 217\u2013233. Springer, Heidelberg (2000)"},{"key":"35_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/3-540-44659-1_15","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2000","unstructured":"Harrison, J.: Formal verification of IA-64 division algorithms. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 234\u2013251. Springer, Heidelberg (2000)"},{"key":"35_CR11","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1023\/A:1022973506233","volume":"22","author":"J. Harrison","year":"2003","unstructured":"Harrison, J.: Formal verification of square root algorithms. Formal Methods in System Design\u00a022, 143\u2013153 (2003)","journal-title":"Formal Methods in System Design"},{"key":"35_CR12","unstructured":"IEEE. Standard for binary floating point arithmetic. ANSI\/IEEE Standard 754-1985, The Institute of Electrical and Electronic Engineers, Inc., 345 East 47th Street, New York, NY 10017, USA (1985)"},{"key":"35_CR13","volume-title":"IA-64 and Elementary Functions: Speed and Precision","author":"P. Markstein","year":"2000","unstructured":"Markstein, P.: IA-64 and Elementary Functions: Speed and Precision. Prentice-Hall, Englewood Cliffs (2000)"},{"key":"35_CR14","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1147\/rd.341.0111","volume":"34","author":"P.W. Markstein","year":"1990","unstructured":"Markstein, P.W.: Computation of elementary functions on the IBM RISC System\/6000 processor. IBM Journal of Research and Development\u00a034, 111\u2013119 (1990)","journal-title":"IBM Journal of Research and Development"},{"key":"35_CR15","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"J.S. Moore","year":"1998","unstructured":"Moore, J.S., Lynch, T., Kaufmann, M.: A mechanically checked proof of the correctness of the kernel of the AMD5 K 86 floating-point division program. IEEE Transactions on Computers\u00a047, 913\u2013926 (1998)","journal-title":"IEEE Transactions on Computers"},{"key":"35_CR16","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1145\/378239.379017","volume-title":"Proceedings of the 38th Design Automation Conference (DAC 2001)","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC 2001), pp. 530\u2013535. ACM Press, New York (2001)"},{"key":"35_CR17","first-page":"1","volume":"1999-Q1","author":"J. O\u2019Leary","year":"1999","unstructured":"O\u2019Leary, J., Zhao, X., Gerth, R., Seger, C.-J.H.: Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal\u00a01999-Q1, 1\u201314 (1999), Available on the Web as, http:\/\/developer.intel.com\/technology\/itj\/q11999\/articles\/art_5.htm .","journal-title":"Intel Technology Journal"},{"key":"35_CR18","series-title":"Lecture Notes in Computer Science","first-page":"195","volume-title":"International Symposium on Programming","author":"J.P. Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent programs in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 195\u2013220. Springer, Heidelberg (1982)"},{"key":"35_CR19","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"D. Rusinoff","year":"1998","unstructured":"Rusinoff, D.: A mechanically checked proof of IEEE compliance of a register-transfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions. LMS Journal of Computation and Mathematics\u00a01, 148\u2013200 (1998), Available on the Web via, http:\/\/www.onr.com\/user\/russ\/david\/k7-div-sqrt.html","journal-title":"LMS Journal of Computation and Mathematics"},{"key":"35_CR20","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.-J.H. Seger","year":"1995","unstructured":"Seger, C.-J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design\u00a06, 147\u2013189 (1995)","journal-title":"Formal Methods in System Design"},{"key":"35_CR21","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/B978-0-08-040953-5.50011-8","volume-title":"Safety of Computer Control Systems SAFECOMP 1990","author":"G. St\u00e5lmarck","year":"1990","unstructured":"St\u00e5lmarck, G., S\u00e4flund, M.: Modeling and verifying systems and software in propositional logic. In: Daniels, B.K. (ed.) Safety of Computer Control Systems SAFECOMP 1990, Gatwick, UK, pp. 31\u201336. Pergamon Press, Oxford (1990)"}],"container-title":["Lecture Notes in Computer Science","FM 2005: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11526841_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:06:56Z","timestamp":1605643616000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11526841_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540278825","9783540317142"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/11526841_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}