{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:01:05Z","timestamp":1725663665138},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540551799"},{"type":"electronic","value":"9783540467632"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55179-4_29","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T04:51:53Z","timestamp":1330231913000},"page":"299-309","source":"Crossref","is-referenced-by-count":6,"title":["A two-level formal verification methodology using HOL and COSMOS"],"prefix":"10.1007","author":[{"given":"Carl -Johan H.","family":"Seger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeffrey J.","family":"Joyce","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,29]]},"reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"W. Bevier, W. Hunt, J Moore, and W. Young, \u201cAn Approach to Systems Verification\u201d, Journal of Automated Reasoning, Vol. 5, No. 4, November 1989.","DOI":"10.1007\/BF00243131"},{"key":"29_CR2","unstructured":"R. Boulton, M. Gordon, J. Herbert and J. Van Tassel, \u201cThe HOL Verification of ELLA Designs\u201d, in: P. Subrahmanyam, ed., Proceedings of a Workshop on Formal Methods in VLSI Design, 9\u201311 January 1991, Miami, Florida."},{"key":"29_CR3","unstructured":"R. S. Boyer and J.S. Moore, A Computational Logic Handbook, Academic Press, 1988."},{"issue":"No.2","key":"29_CR4","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1109\/TC.1984.1676408","volume":"C-33","author":"R. E. Bryant","year":"1984","unstructured":"R.E. Bryant, \u201cA Switch-Level Model and Simulator for MOS Digital Systems,\u201d IEEE Trans. on Computers Vol. C-33, No. 2, February, 1984, pp. 160\u2013177.","journal-title":"IEEE Trans. on Computers"},{"key":"29_CR5","unstructured":"R.E. Bryant, \u201cSymbolic Verification of MOS Circuits\u201d, 1985 Chapel Hill Conference on VLSI, May, 1985, pp. 419\u2013438."},{"key":"29_CR6","volume-title":"DIMAC Workshop on Computer-Aided Verification","author":"R. E. Bryant","year":"1990","unstructured":"R.E. Bryant, and C-J. Seger, \u201cFormal Verification of Digital Circuits Using Symbolic Ternary System Models\u201d, DIMAC Workshop on Computer-Aided Verification, Rutgers, New Jersey, June 18\u201320, 1990 (to appear in Springer Verlag's Lecture Notes in Computer Science)."},{"issue":"No.9","key":"29_CR7","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1109\/32.58786","volume":"SE-16","author":"A. J. Camilleri","year":"1990","unstructured":"Albert John Camilleri, \u201cMechanizing CSP Trace Theory in Higher Order Logic\u201d, IEEE Transactions on Software Engineering, Vol. SE-16, No. 9, September 1990, pp. 993\u20131104.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"No.7","key":"29_CR8","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1109\/2.65","volume":"21","author":"P. Camurati","year":"1988","unstructured":"Paolo Camurati and Paolo Prinetto, \u201cFormal Verification of Hardware Correctness\u201d, IEEE Computer, Vol. 21, No. 7, July 1988, pp. 8\u201319.","journal-title":"IEEE Computer"},{"key":"29_CR9","unstructured":"M. J. C. Gordon, \u201cWhy Higher-Order Logic is a Good Formalism for Specifying and Verifying Hardware\u201d, in: G. Milne and P. Subrahmanyam, eds., Formal Aspects of VLSI Design, Proceedings of the 1985 Edinburgh Conference on VLSI, North-Holland, 1986, pp. 153\u2013177."},{"key":"29_CR10","doi-asserted-by":"crossref","unstructured":"Michael J. C. Gordon, \u201cMechanizing Programming Logics in Higher Order Logic\u201d, in: G. Birtwistle and P. Subrahmanyam, eds., Current Trends in Hardware Verification and Automated Theorem Proving, Springer-Verlag, 1989, pp. 387\u2013439. Also Report No. 145, Computer Laboratory, Cambridge University, September 1988.","DOI":"10.1007\/978-1-4612-3658-0_10"},{"key":"29_CR11","unstructured":"Roger W. S. Hale, Programming in Temporal Logic, Ph.D. Thesis, Report No. 173, Computer Laboratory, Cambridge University, July 1989."},{"key":"29_CR12","series-title":"Report No. 47","volume-title":"Ph.D. Thesis","author":"Warren A. A. Hunt","year":"1985","unstructured":"Warren A. Hunt, FM8501, A Verified Microprocessor, Ph.D. Thesis, Report No. 47, Institute for Computing Science, University of Texas, Austin, December 1985."},{"key":"29_CR13","unstructured":"Jeffrey J. Joyce, \u201cA Verified Compiler for a Verified Microprocessor\u201d, Report No. 167, Computer Laboratory, Cambridge University, March 1989."},{"key":"29_CR14","unstructured":"Jeffrey J. Joyce, \u201cMore Reasons Why Higher-Order Logic is a Good Formalism for Specifying and Verifying Hardware\u201d, in: P. Subrahmanyam, ed., Proceedings of a Workshop on Formal Methods in VLSI Design, 9\u201311 January 1991, Miami, Florida."},{"key":"29_CR15","volume-title":"Specification, Verification and Synthesis: Mathematical Aspects, Proceedings of a Workshop, 5\u20137 July 1989","author":"Jeffrey J. J. Joyce","year":"1989","unstructured":"Jeffrey J. Joyce, \u201cTotally Verified Systems: Linking Verified Software to Verified Hardware\u201d, in: Specification, Verification and Synthesis: Mathematical Aspects, Proceedings of a Workshop, 5\u20137 July 1989, M. Leeser and G. Brown, eds., Ithaca, N.Y., Springer-Verlag, 1989."},{"key":"29_CR16","unstructured":"Michael J. C. Gordon et al., The HOL System Description, Cambridge Research Centre, SRI International, Suite 23, Miller's Yard, Cambridge CB2 1RQ, England."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55179-4_29.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:57:58Z","timestamp":1605628678000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55179-4_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540551799","9783540467632"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-55179-4_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}