{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:50:24Z","timestamp":1725663024124},"publisher-location":"New York, NY","reference-count":15,"publisher":"Springer New York","isbn-type":[{"type":"print","value":"9780387972268"},{"type":"electronic","value":"9780387348018"}],"license":[{"start":{"date-parts":[[1990,1,1]],"date-time":"1990-01-01T00:00:00Z","timestamp":631152000000},"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":[[1990]]},"DOI":"10.1007\/0-387-97226-9_24","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T10:12:03Z","timestamp":1330164723000},"page":"67-89","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Reasoning about state machines in higher-order logic"],"prefix":"10.1007","author":[{"given":"Paul","family":"Loewenstein","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"5_CR1","unstructured":"Mart\u00edn Abadi and Leslie Lamport. The Existence of Refinement Mappings. SRC Report 29, Digital Equipment Corporation, 1988."},{"key":"5_CR2","unstructured":"Robert S. Boyer and J. Strother Moore. A Computational Logic. Academic Press, 1979."},{"key":"5_CR3","unstructured":"Alexandre Bronstein and Carolyn L. Talcott. String-Functional Semantics for Formal Verification of Synchronous Circuits. Report STAN-CS-88-1210, Stanford University Department of Computer Science, 1988."},{"key":"5_CR4","unstructured":"M. C. Browne and E. M. Clarke. SML \u2014 a high level language for the design and verification of finite state machines. In D. Borrione, editor, IFIP International Working Conference: From HDL Descriptions to Guaranteed Circuit Designs, Elsevier Science Publishers B. V. (North-Holland), 1987."},{"key":"5_CR5","unstructured":"Albert Camilleri, Mike Gordon, and Tom Melham. Hardware verification using higher-order logic. In D. Borrione, editor, IFIP International Working Conference: From HDL Descriptions to Guaranteed Circuit Designs, Elsevier Science Publishers B. V. (North-Holland), September 1987."},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Avra. J. Cohn. A proof of correctness of the viper microprocessor: the first level. In G. Birwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_2"},{"key":"5_CR7","unstructured":"Srinivas Devadas, Hi Keung Ma, and A. Richard Newton. On the Verification of Sequential Machines at Differing Levels of Abstraction. Memorandum UCB\/ERL M86\/93, University of California, Berkeley, 1986."},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Michael J.C. Gordon. The denotational semantics of sequential machines. Information Processing Letters, 10(1), February 1980.","DOI":"10.1016\/0020-0190(80)90111-8"},{"key":"5_CR9","unstructured":"Mike Gordon. HOL: A Machine Oriented Formulation of Higher-Order Logic. Technical Report 68, University of Cambridge Computer Laboratory, 1985."},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Mike Gordon. HOL: a proof generating system for higher-order logic. In G. Birwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"5_CR11","unstructured":"Mike Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In G. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI Design, North-Holland, 1986."},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"J. J. Joyce, G. Birtwistle, and M. Gordon. Verification and implementation of a microprocessor. In G. Birwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_4"},{"key":"5_CR13","unstructured":"Paul Loewenstein. The formal verification of state-machines using higher-order logic. In IEEE International Conference on Computer Design, 1989."},{"issue":"3","key":"5_CR14","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"G. L. Peterson","year":"1981","unstructured":"G. L. Peterson. Myths about the mutual exclusion problem. Information Processing Letters, 12(3):115\u2013116, 1981.","journal-title":"Information Processing Letters"},{"key":"5_CR15","unstructured":"Mary Sheeran. \u03bcFP \u2014 An Algebraic VLSI Design Language. Technical Monograph PRG-39, Oxford University Computing Laboratory, 1983."}],"container-title":["Lecture Notes in Computer Science","Hardware Specification, Verification and Synthesis: Mathematical Aspects"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/0-387-97226-9_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T08:12:54Z","timestamp":1558253574000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/0-387-97226-9_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9780387972268","9780387348018"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/0-387-97226-9_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]},"assertion":[{"value":"31 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}