{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T10:39:37Z","timestamp":1742380777767},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540602750"},{"type":"electronic","value":"9783540447849"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60275-5_70","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:05:50Z","timestamp":1330279550000},"page":"261-276","source":"Crossref","is-referenced-by-count":2,"title":["Formal verification of counterflow pipeline architecture"],"prefix":"10.1007","author":[{"given":"Paul N.","family":"Loewenstein","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"18_CR1","first-page":"522","volume-title":"Protocol verification as a hardware design aid","author":"D. L. Dill","year":"1992","unstructured":"David L. Dill, Andreas J. Drexler, Alan J. Hu, and C. Han Yang. Protocol verification as a hardware design aid. In 1992 IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 522\u2013525. IEEE Computer Society, 1992. Cambridge, MA, October 11\u201314."},{"key":"18_CR2","unstructured":"Mike Gordon. HOL: A machine oriented formulation of higher-order logic. Technical Report 68, University of Cambridge Computer Laboratory, 1985."},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Mike Gordon. HOL: A proof generating system for higher-order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis. Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Paul Loewenstein. The formal verification of state-machines using higher-order logic. In IEEE International Conference on Computer Design, pages 204\u2013207. IEEE Computer Society Press, 1989.","DOI":"10.1109\/ICCD.1989.63356"},{"issue":"1\/2","key":"18_CR5","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF01383986","volume":"3","author":"P. Loewenstein","year":"1993","unstructured":"Paul Loewenstein. A formal theory of simulations between infinite automata. Formal Methods in System Design, 3(1\/2):117\u2013149, August 1993.","journal-title":"Formal Methods in System Design"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Paul Loewenstein and David Dill. Formal verification of cache systems using refinement relations. In IEEE International Conference on Computer Design, pages 228\u2013233. IEEE Computer Society Press, 1990.","DOI":"10.1109\/ICCD.1990.130211"},{"key":"18_CR7","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/BF00709156","volume":"1","author":"P. Loewenstein","year":"1992","unstructured":"Paul Loewenstein and David L. Dill. Verification of a multiprocessor cache protocol using simulation relations and higher-order logic. Formal Methods in System Design, 1:355\u2013383, 1992.","journal-title":"Formal Methods in System Design"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Robert F. Sproull, Ivan E. Sutherland, and Charles E. Molnar. Counterflow pipeline processor architecture. IEEE Design and Test of Computers, 11(3), 1994.","DOI":"10.1109\/MDT.1994.303847"}],"container-title":["Lecture Notes in Computer Science","Higher Order Logic Theorem Proving and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60275-5_70.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:35:37Z","timestamp":1619573737000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60275-5_70"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540602750","9783540447849"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-60275-5_70","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}