{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:09:41Z","timestamp":1725664181875},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540600459"},{"type":"electronic","value":"9783540494133"}],"license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60045-0_38","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:37:25Z","timestamp":1330259845000},"page":"31-41","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Hardware verification using monadic second-order logic"],"prefix":"10.1007","author":[{"given":"David A.","family":"Basin","sequence":"first","affiliation":[]},{"given":"Nils","family":"Klarlund","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"4_CR1","volume-title":"Hardware Specification, Verification ana Synthesis: Mathematical Aspects","author":"D. Basin","year":"1989","unstructured":"David Basin and Peter DelVecchio. Verification of combinational logic in Nuprl. In Hardware Specification, Verification ana Synthesis: Mathematical Aspects, Ithaca, New York, 1989. Springer-Verlag."},{"key":"4_CR2","first-page":"43","volume-title":"From HDL Descriptions to Guaranteed Correct Circuit Designs","author":"A. Camilleri","year":"1987","unstructured":"Albert Camilleri, Mike Gordon, and Tom Melham. Hardware verification using higher-order logic. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs, pages 43\u201367. Elsevier Science Publishers B. V. (North-Holland), 1987."},{"key":"4_CR3","unstructured":"Albert John Camilleri. Executing Behavioural Definitions in Higher Order Logic. PhD thesis, University of Cambridge, 1988."},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Cyrluk D., S. Rajan, N. Shankar, and M.K. Srivas. Effective theorem proving for hardware verification. In Second International Conference On Theorem Proving In Circuit Deisgn: Theory, Practice and Experience, Bad Herrenalb, Germany, September 1994.","DOI":"10.1007\/3-540-59047-1_50"},{"key":"4_CR5","unstructured":"1994 Francisco Cantu, Edinburgh DAI. Personal Communication."},{"key":"4_CR6","unstructured":"Michael J. 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. North-Holland, 1986."},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"A. Gupta and Allen L. Fisher. Parametric circuit representation using inductive boolean functions. In C. Courcoubetis, editor, Computer Aided Verification, CAV' 93, LNCS 697, pages 15\u201326. Springer Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_3"},{"key":"4_CR8","unstructured":"A. Gupta and Allen L. Fisher. Tradeoffs in canonical sequential function representations. In Proceedings of the IEEE International Conference on Computer Design, October 1994."},{"key":"4_CR9","unstructured":"F.K. Hanna and N. Daeche. Specification and verification using higher-order logic: a case study. In G.J. Milne and P.A. Subrahmanyam, editors, Formal Aspects of VLSI Design, pages 179\u2013213. Elsevier Science Publishers B.V., 1986."},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"J.G. Henriksen, J. Jensen, M. J\u00f8rgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. Technical Report RS-95-21, BRICS, Department of Computer Science, University of Aarhus, 1995.","DOI":"10.7146\/brics.v2i21.19923"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Hardi Hungar. Combining model checking and theorem proving to verify parallel processes. In C. Courcoubetis, editor, Computer Aided Verification, CAV' 93, LNCS 697, pages 154\u2013165. Springer Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_13"},{"issue":"4","key":"4_CR12","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1007\/BF00243132","volume":"5","author":"W. Hunt","year":"1989","unstructured":"Warren Hunt. Microprocessor design verification. Journal of Automated Reasoning, 5(4):429\u2013460, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR13","first-page":"89","volume-title":"From HDL Descriptions to Guaranteed Correct Circuit Designs","author":"W. J. Hunt","year":"1987","unstructured":"Warren J. Hunt. The mechanical verification of a microprocessor design. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs, pages 89\u2013129. Elsevier Science Publishers B. V. (North-Holland), 1987."},{"key":"4_CR14","unstructured":"M. Morris Mano. Digital logic and computer design. Prentice-Hall, Inc., 1979."},{"key":"4_CR15","unstructured":"T. F. Melham. Using recursive types of reasoning about hardware in higher order logic. In International Working Conference on The fusion of Hardware Design and Verification, pages 26\u201349, July 1988."},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"J.-K. Rho. and F. Somenzi. Automatic generation of network invariants for the verification of iterative sequential networks. In C. Courcoubetis, editor, Computer Aided Verification, CAV' 93, LNCS 697, pages 123\u2013137. Springer Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_11"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 133\u2013191. MIT Press\/Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60045-0_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T08:19:44Z","timestamp":1558253984000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60045-0_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600459","9783540494133"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-60045-0_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]},"assertion":[{"value":"31 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}