{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T13:59:35Z","timestamp":1742392775163},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[1992,12,1]],"date-time":"1992-12-01T00:00:00Z","timestamp":723168000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1992,12]]},"DOI":"10.1007\/bf00709156","type":"journal-article","created":{"date-parts":[[2004,12,1]],"date-time":"2004-12-01T04:41:38Z","timestamp":1101876098000},"page":"355-383","source":"Crossref","is-referenced-by-count":6,"title":["Verification of a multiprocessor cache protocol using simulation relations and higher-order logic"],"prefix":"10.1007","volume":"1","author":[{"given":"Paul N.","family":"Loewesstein","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":"CR1","volume-title":"VLSI Specification, Verification and Synthesis","author":"Avra J Cohn","year":"1988","unstructured":"Avra. J.Cohn. A proof of correctness of the Viper microprocessor: The first level. InVLSI Specification, Verification and Synthesis, G.Birtwistle and P.A.Subrahmanyam (eds.). Kluwer Academic Publishers, Boston, 1988."},{"key":"CR2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-1-4612-3658-0_1","volume-title":"Current Trends in Hardware Verification and Automated Theorem Proving","author":"Avra Cohn","year":"1989","unstructured":"AvraCohn. Correctness properties of the Viper block model: The second level. InCurrent Trends in Hardware Verification and Automated Theorem Proving, G.Birtwistle and P.A.Subrahmanyam (eds.). Springer-Verlag, New York, 1989, pp. 1?91."},{"key":"CR3","volume-title":"HDL Descriptions to Guaranteed Correct Circuit Designs","author":"W.A. Hunt Jr.","year":"1987","unstructured":"W.A.HuntJr. The mechanical verification of a microprocessor design. InHDL Descriptions to Guaranteed Correct Circuit Designs, D.Borrione (ed.) North Holland, Amsterdam, 1987."},{"key":"CR4","volume-title":"Current Trends in Hardware Verification and Automated Theorem Proving","author":"Paliath Narendran","year":"1989","unstructured":"PaliathNarendran and JonathanStillman. Formal verification of the sobel image processing chip. InCurrent Trends in Hardware Verification and Automated Theorem Proving, G.Birtwistle and P.A.Subrahmanyam (eds.). Springer-Verlag, New York, 1989."},{"issue":"2","key":"CR5","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"Martin Abadi","year":"1991","unstructured":"MartinAbadi and LeslieLamport. The existence of refinement mappings.Theoretical Computer Science, 82(2):253?284, May 1991.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"CR6","first-page":"137","volume":"10","author":"Simon S. Lam","year":"1984","unstructured":"Simon S.Lam and A. UdayaShankar. Protocol verification via projections.IEEE Transactions on Software Engineering, SE-10(2):137?151, July 1984.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"CR7","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":"CR8","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan. Analysis of discrete event coordination. InStepwise Refinement of Distributed Systems, J.W. de Bakker, W.P. De Roever, and G. Rozenberg, (eds.).Lecture Notes in Computer Science, 430:1990.","DOI":"10.1007\/3-540-52559-9_74"},{"key":"CR9","unstructured":"R. Milner. An algebraic definition of simulation between programs. InProceedings 2nd International Joint Conference on Artificial Intelligence, 1971."},{"key":"CR10","unstructured":"Nils Klarlund and Fred B. Schneider. Verifying safety properties using non-deterministic infinitestate automata. Technical Report TR 89-1037, Cornell University Computer Science Department, 1989."},{"key":"CR11","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."},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow. Formal verification of data type refinement. InStepwise Refinement of Distributed Systems, J.W. de Bakker, W.P. De Roever, and G. Rozenberg, (eds.).Lecture Notes in Computer Science, 430:1990.","DOI":"10.1007\/3-540-52559-9_79"},{"issue":"12","key":"CR13","doi-asserted-by":"crossref","first-page":"1035","DOI":"10.1109\/TC.1986.1676711","volume":"35","author":"Michael C. Browne","year":"1986","unstructured":"Michael C.Browne, Edmund M.Clarke, David L.Dill, and BudMishra. Automatic verification of sequential circuits using temporal logic.IEEE Transactions on Computers, C-35(12):1035?1044, December 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"CR14","volume-title":"IFIP Sixth Computer Hardware Description Languages and their Applications","author":"Masahirio Fujita","year":"1983","unstructured":"MasahirioFujita, HedehikoTanaka, and TohruMoto-oka. Verification with prolog and temporal logic. InIFIP Sixth Computer Hardware Description Languages and their Applications, T.Uehara and M.Barbacci, (eds.) North Holland Publishing Company, Amsterdam, 1983."},{"key":"CR15","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/6874.001.0001","volume-title":"Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits","author":"David L. Dill","year":"1989","unstructured":"David L.Dill.Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. MIT Press, Cambridge, MA, 1989."},{"key":"CR16","unstructured":"Mike Gordon. HOL: A machine oriented formulation of higher-order logic. Technical Report 68, University of Cambridge Computer Laboratory, 1985."},{"key":"CR17","volume-title":"VLSI Specification, Verification and Synthesis","author":"Mike Gordon","year":"1988","unstructured":"MikeGordon. HOL: A proof generating system for higher-order logic. InVLSI Specification, Verification and Synthesis, G.Birtwistle and P. A.Subrahmanyam (eds.). Kluwer Academic Publishers, Boston, 1988."},{"key":"CR18","unstructured":"Konrad Slind. An implementation of higher order logic. Research Report 91\/419\/03, University of Calgary, January 1991."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00709156.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00709156\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00709156","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T12:20:34Z","timestamp":1586002834000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00709156"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,12]]},"references-count":18,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1992,12]]}},"alternative-id":["BF00709156"],"URL":"https:\/\/doi.org\/10.1007\/bf00709156","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,12]]}}}