{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T05:19:41Z","timestamp":1737609581130,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540657033"},{"type":"electronic","value":"9783540490593"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-49059-0_23","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T21:56:57Z","timestamp":1194991017000},"page":"330-344","source":"Crossref","is-referenced-by-count":1,"title":["A Light-Weight Framework for Hardware Verification"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Kern","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tarik","family":"Ono-Tesfaye","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark R.","family":"Greenstreet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,3,12]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Mark Aagaard and Carl-Johan H. Seger. The formal verification of a pipelined double-precision IEEE floating-point multiplier. In Int. Conf. on Computer-Aided Design, ICCAD\u2019 95, pages 7\u201310, November 1995.","DOI":"10.1109\/ICCAD.1995.479878"},{"issue":"2","key":"23_CR2","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"Mart\u00edn Abadi and Leslie Lamport. The existence of refinement mappings. Theor. Comput. Sci., 82(2):253\u2013284, May 1991.","journal-title":"Theor. Comput. Sci."},{"key":"23_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0031985","volume-title":"Proceedings of the REX Workshop, \u201cReal-Time: Theory in Practice\u201d","author":"M. Abadi","year":"1992","unstructured":"Mart\u00edn Abadi and Leslie Lamport. An old-fashioned recipe for real time. In J. W. de Bakker et al., editors, Proceedings of the REX Workshop, \u201cReal-Time: Theory in Practice\u201d. Springer, 1992. LNCS 600."},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Andrew W. Appel and David B. MacQueen. Standard ML of New Jersey. In 3rd Int. Symp. on Prog. Lang. Implement. and Logic Program., number 528 in Lect. Notes Comput. Sci., pages 1\u201313. Springer-Verlag, August 1991.","DOI":"10.1007\/3-540-54444-5_83"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"N. Bj\u00f8rner, A. Browne, E. Chang, M. Col\u00f3n, A. Kapur, Z. Manna, H. B. Sipma, and T. E. Uribe. STeP: Deductive-algorithmic verification of reactive and real-time systems. In 8th Int. Conf. Computer-Aided Verification, CAV\u2019 96, number 1102 in Lect. Notes Comput. Sci., pages 415\u2013418. Springer-Verlag, August 1996.","DOI":"10.1007\/3-540-61474-5_92"},{"key":"23_CR6","unstructured":"Richard Boulton, Andrew Gordon, Mike Gordon, John Harrison, John Herbert, and John Van Tassel. Experience with embedding hardware description languages in HOL. In 1st Int. Conf. on Theorem Provers in Circuit Design, TPCD\u2019 92, pages 129\u2013156. North Holland, 1992."},{"key":"23_CR7","volume-title":"Digital computer arithmetic: design and implementation","author":"J. J. F. Cavanagh","year":"1984","unstructured":"Joseph J. F. Cavanagh. Digital computer arithmetic: design and implementation. McGraw-Hill, New York, 1984."},{"key":"23_CR8","unstructured":"E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976."},{"key":"23_CR9","unstructured":"Michael Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In G. J. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI Design, pages 153\u2013177. Elsevier Science Publishers, 1985."},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Michael J. C. Gordon. HOL: a proof generating system for higher-order logic. In Graham Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 74\u2013128. Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"23_CR11","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/BF01384079","volume":"4","author":"C. Harkness","year":"1994","unstructured":"Cheryl Harkness and Elizabeth Wolf. Verifying the Summit bus converter protocols with symbolic model checking. Formal Meth. System Design, 4:83\u201397, 1994.","journal-title":"Formal Meth. System Design"},{"issue":"4","key":"23_CR12","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1109\/43.372367","volume":"14","author":"S. Hazelhurst","year":"1995","unstructured":"Scott Hazelhurst and Carl-Johan H. Seger. A simple theorem prover based on symbolic trajectory evaluation and BDDs. IEEE Trans. Comput. Aided Des. Integr. Circuits, 14(4):413\u2013422, April 1995.","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits"},{"issue":"3","key":"23_CR13","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1145\/78969.78970","volume":"12","author":"L. Lamport","year":"1990","unstructured":"Leslie Lamport. win and sin: Predicate transformers for concurrency. ACM Trans. Program. Lang. Syst., 12(3):396\u2013428, July 1990.","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"23_CR14","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Greg Nelson and Derek C. Oppen. Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst., 1(2):245\u2013257, October 1979.","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Tarik Ono-Tesfaye, Christoph Kern, and Mark R. Greenstreet. Verifying a self-timed divider. In Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems. IEEE Computer Society Press, April 1998.","DOI":"10.1109\/ASYNC.1998.666501"},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In 11th Int. Conf. Automated Deduction (CADE\u2019 92), number 607 in Lect. Notes Comput. Sci., pages 748\u2013752. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"23_CR17","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Number 828 in Lect. Notes Comput. Sci. Springer-Verlag, Berlin, 1994."},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Amir Pnueli and Elad Shahar. A platform for combining deductive with algorithmic verificication. In 8th Int. Conf. Computer-Aided Verification, CAV\u2019 96, number 1102 in Lect. Notes Comput. Sci., pages 184\u2013195. Springer-Verlag, August 1996.","DOI":"10.1007\/3-540-61474-5_68"},{"key":"23_CR19","doi-asserted-by":"crossref","unstructured":"F. Pong, A. Nowatzyk, G. Aybay, and M. Dubois. Verifying distributed directory-based cache coherence protocols: S3.mp, a case study. In Proc. EURO-Par\u2019 95 Parallel Processing, number 966 in Lect. Notes Comput. Sci., pages 287\u2013300. Springer-Verlag, August 1995.","DOI":"10.1007\/BFb0020472"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"S. Rajan, N. Shankar, and M. K. Srivas. An integration of model-checking with automated proof checking. In 7th Int. Conf. Computer-Aided Verification, CAV\u2019 95, number 939 in Lect. Notes Comput. Sci., pages 84\u201397. Springer-Verlag, July 1995.","DOI":"10.1007\/3-540-60045-0_42"},{"key":"23_CR21","unstructured":"Charles L. Seitz. System timing. In Carver Mead and Lynn Conway, editors, Introduction to VLSI Systems, pages 218\u2013262. Addison-Wesley, 1980."},{"issue":"1","key":"23_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. E. Shostak","year":"1984","unstructured":"Robert E. Shostak. Deciding combinations of theories. J. ACM, 31(1):1\u201312, January 1984.","journal-title":"J. ACM"},{"key":"23_CR23","unstructured":"Fabio Somenzi. CUDD: CU Decision Diagram Package. URL: http:\/\/bessie.colorado.edu\/~fabio\/CUDD\/cuddIntro.html ."},{"issue":"2","key":"23_CR24","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/BF00122419","volume":"8","author":"M. K. Srivas","year":"1996","unstructured":"Mandayam K. Srivas and Steven P. Miller. Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods. Formal Meth. System Design, 8(2):153\u2013188, March 1996.","journal-title":"Formal Meth. System Design"},{"key":"23_CR25","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-2764-0","volume-title":"A formal approach to hardware design","author":"J. Staunstrup","year":"1994","unstructured":"J\u00f8rgen Staunstrup. A formal approach to hardware design. Kluwer Academic Publishers, Boston, 1994."},{"key":"23_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01788562","volume":"3","author":"T. Verhoeff","year":"1988","unstructured":"Tom Verhoeff. Delay-insensitive codes-an overview. Distributed Computing, 3:1\u20138, 1988.","journal-title":"Distributed Computing"},{"key":"23_CR27","unstructured":"T. E. Williams, M. A. Horowitz, R. L. Alverson, and T. S. Yang. A self-timed chip for division. In Stanford Conference on Advanced Research in VLSI, pages 75\u201396, March 1987."},{"key":"23_CR28","series-title":"Technical Report","volume-title":"Self-timed rings and their application to division","author":"T. E. Williams","year":"1991","unstructured":"Ted E. Williams. Self-timed rings and their application to division. Technical Report CSL-TR-91-482, Computer Systems Lab, Dept. of EE, Stanford, May 1991."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49059-0_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T08:33:35Z","timestamp":1737534815000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49059-0_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540657033","9783540490593"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-49059-0_23","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}