{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:46Z","timestamp":1725663826681},"publisher-location":"Berlin, Heidelberg","reference-count":7,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540578260"},{"type":"electronic","value":"9783540483465"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57826-9_159","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:27:29Z","timestamp":1330262849000},"page":"501-513","source":"Crossref","is-referenced-by-count":0,"title":["Verification in higher order logic of mutual exclusion algorithm"],"prefix":"10.1007","author":[{"given":"Victor A.","family":"Carre\u00f1o","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Martin Abadi and Leslie Lamport, An Old-Fashioned Recipe for Real Time, in proceedings 1991 Rex Workshop, Real-time: Theory in Practice, J.W. de Bakker et al., editors, Springer-Verlag, 1992.","key":"39_CR1","DOI":"10.1007\/BFb0031985"},{"unstructured":"Victor Carre\u00f1o, The Transition Assertions Specification Method, University of Cambridge Computer Laboratory, Technical Report No. 279, January 1993.","key":"39_CR2"},{"doi-asserted-by":"crossref","unstructured":"Avra Cohen, Correctness Properties of the Viper Microprocessor: The Second Level, in: Current Trends in Hardware Verification and Automated Theorem Proving, edited by G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, 1989, Pages 1\u201391.","key":"39_CR3","DOI":"10.1007\/978-1-4612-3658-0_1"},{"issue":"no.1","key":"39_CR4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/7351.7352","volume":"5","author":"L. Lamport","year":"1987","unstructured":"Leslie Lamport, A Fast Mutual Exclusion Algorithm ACM transactions on Computer Systems, Vol. 5 no. 1, February 1987, Pages 1\u201311.","journal-title":"ACM transactions on Computer Systems"},{"unstructured":"Thomas Melham, Formalizing Abstraction Mechanisms for Hardware Verfication in Higher Oreder Logic, University of Cambridge Computer Laboratory, Technical Report No. 201, August 1990.","key":"39_CR5"},{"unstructured":"Fred Schneider, Bard Bloom, and Keith Marzullo, Putting Time Into Proof Outlines Cornell University, Department of Computer Science Technical Report TR 91-1238, September 1991.","key":"39_CR6"},{"unstructured":"N. Shankar, Mechanized Verification of Real-Time Systems Using PVS SRI International Computer Science Laaboratory Technical Report SRI-CSL-92-12, November 1992.","key":"39_CR7"}],"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-57826-9_159.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:14:33Z","timestamp":1605647673000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57826-9_159"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578260","9783540483465"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/3-540-57826-9_159","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}