{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T23:25:19Z","timestamp":1773098719072,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540678632","type":"print"},{"value":"9783540446590","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44659-1_21","type":"book-chapter","created":{"date-parts":[[2007,7,21]],"date-time":"2007-07-21T13:40:26Z","timestamp":1185025226000},"page":"338-355","source":"Crossref","is-referenced-by-count":25,"title":["Divider Circuit Verification with Model Checking and Theorem Proving"],"prefix":"10.1007","author":[{"given":"Roope","family":"Kaivola","sequence":"first","affiliation":[]},{"given":"Mark D.","family":"Aagaard","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"M. D. Aagaard, R. B. Jones, K. R. Kohatsu, R. Kaivola, and C.-J. H. Seger. Formal verification of iterative algorithms in microprocessors. In DAC, June 2000.","DOI":"10.1145\/337292.337388"},{"key":"21_CR2","volume-title":"Theorem Proving in Higher Order Logics","author":"M. D. Aagaard","year":"1999","unstructured":"M. D. Aagaard, R. B. Jones, and C.-J. H. Seger. Lifted-fl: A pragmatic implementation of combined model checking and theorem proving. In L. Thery, editor, Theorem Proving in Higher Order Logics. Springer Verlag; New York, Sept. 1999."},{"key":"21_CR3","volume-title":"CHARME","author":"M. D. Aagaard","year":"1999","unstructured":"M. D. Aagaard, T. F. Melham, and O. J. W. Xs are for trajectory evaluation, Booleans are for theorem proving. In CHARME. Springer Verlag; New York, Oct. 1999."},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"R. E. Bryant. Bit-level analysis of an SRT divider circuit. In DAC, pages 661\u2013665, New York, June 1996. ACM.","DOI":"10.21236\/ADA294842"},{"key":"21_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/BFb0031797","volume-title":"Formal Methods in CAD","author":"Y.-A. Chen","year":"1996","unstructured":"Y.-A. Chen, E. Clarke, P.-H. Ho, Y. Hoskote, T. Kam, M. Khaira, J. O\u2019Leary, and X. Zhao. Verification of all circuits in a floating-point unit using word-level model checking. In M. Srivas and A. Camilleri, editors, Formal Methods in CAD, volume 1166 of LNCS, pages 19\u201333, Palo Alto, CA, USA, Nov. 1996. Springer Verlag; New York."},{"key":"21_CR6","volume-title":"CAV","author":"C.-T. Chou","year":"1999","unstructured":"C.-T. Chou. The mathematical foundation of symbolic trajectory evaluation. In CAV. Springer Verlag; New York, 1999."},{"key":"21_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/3-540-61474-5_62","volume-title":"CAV","author":"E. M. Clarke","year":"1996","unstructured":"E. M. Clarke, S. M. German, and X. Zhao. Verifying the SRT division algorithm using theorem proving techniques. In Rajeev Alur and Thomas A. Henzinger, editors, CAV, volume 1102 of LNCS, pages 111\u2013122, New Brunswick, NJ, USA, July\/Aug. 1996. Springer Verlag; New York."},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, M. Khaira, and X. Zhao. Word level model checking-avoiding the Pentium FDIV error. In DAC, pages 645\u2013648, New York, June 1996. ACM.","DOI":"10.1145\/240518.240640"},{"key":"21_CR9","unstructured":"M. D. Ercegovac and T. Lang. Division and Square Root, Digit-Recurrence Algorithms and Implementations. Kluwer Academic, 1994."},{"key":"21_CR10","unstructured":"M. Gordon. Programming combinations of deduction and BDD-based symbolic calculation. Technical Report 480, Cambridge Comp. Lab, 1999."},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"D. Gries. The Science of Programming. Springer-Verlag, 1981.","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"21_CR12","doi-asserted-by":"crossref","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":"J. Harrison. A machine-checked theory of floating point arithmetic. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. The\u0155y, editors, Theorem Proving in Higher Order Logics, pages 113\u2013130. Springer Verlag; New York, Sept. 1999."},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"S. Hazelhurst and C.-J. H. Seger. A simple theorem prover based on symbolic trajectory evaluation and BDDs. IEEE Trans. on CAD, Apr. 1995.","DOI":"10.1109\/43.372367"},{"key":"21_CR14","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/3-540-63475-4_1","volume-title":"Formal Hardware Verification","author":"S. Hazelhurst","year":"1997","unstructured":"S. Hazelhurst and C.-J. H. Seger. Symbolic trajectory evaluation. In T. Kropf, editor, Formal Hardware Verification, chapter 1, pages 3\u201378. Springer Verlag; New York, 1997."},{"key":"21_CR15","unstructured":"IEEE. IEEE Standard for binary floating-point arithmetic. ANSI\/IEEE Std 754-1985, 1985."},{"key":"21_CR16","first-page":"68","volume-title":"Designing Correct Circuits","author":"J. Joyce","year":"1990","unstructured":"J. Joyce. Generic specification of digital hardware. In G. Jones and M. Sheeran, editors, Designing Correct Circuits, pages 68\u201391. Springer Verlag; New York, Sept. 1990."},{"key":"21_CR17","unstructured":"A. Kaldewaij. Programming: The Derivation of Algorithms. Prentice-Hall, 1990."},{"issue":"9","key":"21_CR18","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"J. S. Moore","year":"1998","unstructured":"J. S. Moore, T. W. Lynch, and M. Kaufmann. A mechanically checked proof of the AMD K-5 86 floating point division program. IEEE Trans. on Comp., 47(9):913\u2013926, Sept. 1998.","journal-title":"IEEE Trans. on Comp."},{"key":"21_CR19","unstructured":"J. O\u2019Leary, X. Zhao, R. Gerth, and C.-J. H. Seger. Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal, Q1, Feb. 1999."},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"L. Paulson. ML for the Working Programmer, Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511811326"},{"key":"21_CR21","series-title":"International Series in Computer Science","volume-title":"The Implementation of Functional Programming Languages","author":"S. L. Peyton Jones","year":"1987","unstructured":"S. L. Peyton Jones. The Implementation of Functional Programming Languages. International Series in Computer Science. Prentice Hall, New York, 1987."},{"key":"21_CR22","first-page":"148","volume":"1","author":"D. M. Russinoff","year":"1998","unstructured":"D. M. Russinoff. A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor. J. of Comp. Math., 1:148\u2013200, 1998. London Math. Soc.","journal-title":"J. of Comp. Math."},{"issue":"2","key":"21_CR23","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.-J. H. Seger","year":"1995","unstructured":"C.-J. H. Seger and R. E. Bryant. Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design, 6(2): 147\u2013189, Mar. 1995.","journal-title":"Formal Methods in System Design"},{"key":"21_CR24","first-page":"32","volume-title":"Theorem Provers in Circuit Design","author":"P. J. Windley","year":"1994","unstructured":"P. J. Windley and M. Coe. A correctness model for pipelined microprocessors. In R. Kumar and T. Kropf, editors, Theorem Provers in Circuit Design, pages 32\u201351. Springer Verlag; New York, 1994."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44659-1_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T07:32:59Z","timestamp":1556695979000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44659-1_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678632","9783540446590"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-44659-1_21","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]}}}