{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:14:47Z","timestamp":1725455687915},"publisher-location":"Berlin\/Heidelberg","reference-count":19,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540544771"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0023744","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T06:01:03Z","timestamp":1132380063000},"page":"302-311","source":"Crossref","is-referenced-by-count":6,"title":["Verification of a multiprocessor cache protocol using simulation relations and higher-order logic (summary)"],"prefix":"10.1007","author":[{"given":"Paul","family":"Loewenstein","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"32_CR1","unstructured":"Mart\u00edn Abadi and Leslie Lamport. The existence of refinement mappings. SRC Report 29, Digital Equipment Corporation, 1988."},{"issue":"12","key":"32_CR2","doi-asserted-by":"crossref","first-page":"1035","DOI":"10.1109\/TC.1986.1676711","volume":"C-35","author":"M. C. Browne","year":"1986","unstructured":"Michael C. Browne, Edmund M. Clarke, David L. Dill, and Bud Mishra. Automatic verification of sequential circuits using temporal logic. IEEE Transactions on Computers, C-35(12):1035\u20131044, December 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"Avra Cohn. Correctness properties of the Viper block model: The second level. In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 1\u201391. Springer-Verlag, 1989.","DOI":"10.1007\/978-1-4612-3658-0_1"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"Avra. J. Cohn. A proof of correctness of the Viper microprocessor: The first level. 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_2"},{"key":"32_CR5","volume-title":"On the verification of sequential machines at differing levels of abstraction","author":"S. Devadas","year":"1986","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":"32_CR6","doi-asserted-by":"crossref","unstructured":"David L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. MIT Press, 1989.","DOI":"10.7551\/mitpress\/6874.001.0001"},{"key":"32_CR7","unstructured":"Masahirio Fujita, Hedehiko Tanaka, and Tohru Moto-oka. Verification with prolog and temporal logic. In T. Uehara and M. Barbacci, editors, IFIP Sixth Computer Hardware Description Languages and their applications, pages 103\u2013114. North Holland Publishing Company, 1983."},{"key":"32_CR8","unstructured":"Mike Gordon. HOL: A machine oriented formulation of higher-order logic. Technical Report 68, University of Cambridge Computer Laboratory, 1985."},{"key":"32_CR9","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":"32_CR10","unstructured":"W. A. Hunt, Jr. The mechanical verification of a microprocessor design. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs. North Holland, 1987."},{"key":"32_CR11","unstructured":"Nils Klarlund and Fred B. Schneider. Verifying safety properties using non-deterministic infinite-state automata. Technical Report TR 89-1037, Cornell University Computer Science Department, 1989."},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan. Analysis of discrete event coordination. In J.W. de Bakker, W.-P. De Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52559-9_74"},{"issue":"2","key":"32_CR13","first-page":"137","volume":"SE-10","author":"S. S. Lam","year":"1984","unstructured":"Simon S. Lam and A. Udaya Shankar. Protocol verification via projections. IEEE transactions on software engineering, SE-10(2):137\u2013151, July 1984.","journal-title":"IEEE transactions on software engineering"},{"key":"32_CR14","doi-asserted-by":"crossref","unstructured":"Paul Loewenstein. Reasoning about state-machines in higher-order logic. In M. Leeser and G. Brown, editors, Hardware Specification, Verification and Synthesis: Mathematical Aspects. Springer Verlag, 1990.","DOI":"10.1007\/0-387-97226-9_24"},{"key":"32_CR15","doi-asserted-by":"crossref","unstructured":"Paul Loewenstein and David L. Dill. Verification of a multiprocessor cache protocol using simulation relations and higher-order logic. In Computer-Aided Verification (Proceedings of the CAV90 Workshop), volume 3 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, 1991.","DOI":"10.1090\/dimacs\/003\/14"},{"key":"32_CR16","doi-asserted-by":"crossref","unstructured":"Nancy A. Lynch and Mark R. Tuttle. Hierarchical correctness proofs for distributed algorithms. Technical Report TR-387, MIT Laboratory for Computer Science, 1987.","DOI":"10.1145\/41840.41852"},{"key":"32_CR17","doi-asserted-by":"crossref","unstructured":"Paliath Narendran and Jonathan Stillman. Formal verification of the sobel image processing chip. In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 92\u2013107. Springer-Verlag, 1989.","DOI":"10.1007\/978-1-4612-3658-0_2"},{"key":"32_CR18","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow. Formal verification of data type refinement. In J.W. de Bakker, W.-P. De Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52559-9_79"},{"key":"32_CR19","unstructured":"A. P. Sistla. A complete proof system for proving correctness of non-deterministic safety specifications. Technical Report TC-0060-8-89-378, GTE Laboratories, 1989."}],"container-title":["Lecture Notes in Computer Science","Computer-Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0023744","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T01:26:45Z","timestamp":1586568405000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0023744"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540544771"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0023744","relation":{},"subject":[]}}