{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:09:44Z","timestamp":1725487784130},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678632"},{"type":"electronic","value":"9783540446590"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44659-1_28","type":"book-chapter","created":{"date-parts":[[2007,7,21]],"date-time":"2007-07-21T17:40:26Z","timestamp":1185039626000},"page":"443-461","source":"Crossref","is-referenced-by-count":3,"title":["Formal Verification of the Alpha 21364 Network Protocol"],"prefix":"10.1007","author":[{"given":"Abdel","family":"Mokkedem","sequence":"first","affiliation":[]},{"given":"Tim","family":"Leonard","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","unstructured":"Peter Bannon. Alpha 21364: a scalable single-chip SMP. In Microprocessor Forum (Cahners MicroDesign Resources), pages 68\u201380, October 1998. \n                  http:\/\/www.digital.com\/alphaoem\/present\/index.htm\n                  \n                ."},{"key":"28_CR2","unstructured":"[BBJ+95]_M. Bass, T.W. Blanchard, D.D. Josephson, D. Weir, and D.L. Halperin. Design methodologies for the PA 7100LC microprocessor. Hewlett-Packard Journal, 1995."},{"key":"28_CR3","unstructured":"Ricky W. Butler and Jon A. Sjogren. A PVS Graph Theory Library. Technical Report Memorandum, NASA Langly Research Center, December 1997. \n                  http:\/\/atb-www.larc.nasa.gov\/ftp\/larc\/PVS-library\n                  \n                ."},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"W.J. Dally and C.L. Seitz. Deadlock-free message routing in multiprocessor interconnection networks. IEEE Transactions on Computers, 1987.","DOI":"10.1109\/TC.1987.1676939"},{"key":"28_CR5","unstructured":"Mike Kantrowitz and Lisa M. Noack. Functional verification of a multi-issue, pipelined, superscalar Alpha processor-the Alpha 21164 CPU chip. Digital Technical Journal, 1995."},{"key":"28_CR6","unstructured":"Leslie Lamport. Specifying concurrent systems with TLA+. In Manfred. Broy and Ralf Steinbr\u00fcggen, editors, Calculational System Design, pages 183\u2013247. IOS Press, 1999."},{"key":"28_CR7","unstructured":"K.L. McMillan. Getting started with SMV. Technical report, Cadence Berkeley Labs, December 1999. \n                  http:\/\/www-cad.eecs.berkeley.edu:80\/~kenmcmil\/\n                  \n                ."},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"A. Mokkedem, R. Hosabettu, M.D. Jones, and G. Gopalakrishan. Formalization and analysis of a solution to the PCI 2.1 bus transaction ordering problem. Formal Methods in System Design, 2000.","DOI":"10.1023\/A:1008729625855"},{"key":"28_CR9","volume-title":"PVS Tutorial","author":"N. Shankar","year":"1993","unstructured":"N. Shankar, S. Owre, and J. M. Rushby. PVS Tutorial. Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993. Also appears in Tutorial Notes, Formal Methods Europe\u2019 93: Industrial-Strength Formal Methods, pages 357\u2013406, Odense, Denmark, April 1993."},{"key":"28_CR10","first-page":"638","volume-title":"Design Automation Conference, DAC\u2019 98","author":"T. A. Taylor","year":"1998","unstructured":"[TQB+98]_Scott A. Taylor, Michael Quinn, Darren Brown, Nathan Dohm, Scot Hildebrandt, James Huggins, and Carl Ramey. Functional verification of a multiple-issue, out-of-order, superscalar Alpha processor-the DEC Alpha 21264 microprocessor. In Design Automation Conference, DAC\u2019 98, pages 638\u2013643, Moscone center, San Francico, California, USA, June 1998. Association for Computing Machinery."},{"key":"28_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods","author":"Y. Yu","year":"1999","unstructured":"Yuan Yu, Panagiotis Manolios, and Leslie Lamport. Model checking TLA+ specifications. In Laurence Pierre and Thomas Kropf, editors, Correct Hardware Design and Verification Methods, LNCS, pages 54\u201366. Springer-Verlag, September 1999."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44659-1_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,10,8]],"date-time":"2018-10-08T16:39:20Z","timestamp":1539016760000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44659-1_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678632","9783540446590"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-44659-1_28","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}