{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,4]],"date-time":"2026-10-04T16:42:24Z","timestamp":1791132144543,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540603856","type":"print"},{"value":"9783540455165","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60385-9_2","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:24:01Z","timestamp":1330280641000},"page":"21-34","source":"Crossref","is-referenced-by-count":31,"title":["Automatic verification of the SCI cache coherence protocol"],"prefix":"10.1007","author":[{"given":"Ulrich","family":"Stern","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In 27th ACM\/IEEE Design Automation Conference, pages 46\u201351, 1990.","DOI":"10.1145\/123186.123223"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"D. L. Dill, A. J. Drexler, A. J. Hu, and C. H. Yang. Protocol verification as a hardware design aid. In IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 522\u20135, 1992.","DOI":"10.1109\/ICCD.1992.276232"},{"key":"2_CR3","unstructured":"D. L. Dill, S. Park, and A. G. Nowatzyk. Formal specification of abstract memory models. In Symposium on Research on Integrated Systems, pages 38\u201352, 1993."},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"S. Gjessing, S. Krogdahl, and E. Munthe-Kaas. A top down approach to the formal specification of SCI cache coherence. In Computer Aided Verification. 3rd International Workshop, pages 83\u201391, 1991.","DOI":"10.1007\/3-540-55179-4_9"},{"key":"2_CR5","unstructured":"S. Gjessing and E. Munthe-Kaas. Formal specification of cache coherence in a shared memory multiprocessor. Research Report 158, Department of Informatics, University of Oslo, 1991."},{"issue":"1","key":"2_CR6","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/40.124376","volume":"12","author":"D. B. Gustavson","year":"1992","unstructured":"D. B. Gustavson. The Scalable Coherent Interface and related standards projects. IEEE Micro, 12(1):10\u201322, 1992.","journal-title":"IEEE Micro"},{"key":"2_CR7","unstructured":"IEEE Std 1596\u20131992, IEEE Standard for Scalable Coherent Interface (SCI)."},{"key":"2_CR8","unstructured":"C. N. Ip and D. L. Dill. Better verification through symmetry. In 11th International Conference on Computer Hardware Description Languages and their Applications, pages 97\u2013111, 1993."},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"C. N. Ip and D. L. Dill. Efficient verification of symmetric concurrent systems. In IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 230\u2013234, 1993.","DOI":"10.1109\/ICCD.1993.393375"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"D. V. James. The Scalable Coherent Interface: Scaling to high-performance systems. In Spring COMPCON, pages 64\u201371, 1994.","DOI":"10.1109\/CMPCON.1994.282943"},{"issue":"6","key":"2_CR11","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1109\/2.55503","volume":"23","author":"D. V. James","year":"1990","unstructured":"D. V. James, A. T. Laundrie, S. Gjessing, and G. S. Sohi. Distributed-directory scheme: Scalable Coherent Interface. Computer, 23(6):74\u20137, 1990.","journal-title":"Computer"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"C. Jard and T. J\u00e9ron. Bounded-memory algorithms for verification on-the-fly. In Computer Aided Verification. 3rd International Workshop, pages 192\u2013202, 1991.","DOI":"10.1007\/3-540-55179-4_19"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"U. Stern and D. L. Dill. Improved probabilistic verification by hash compaction. In IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, 1995.","DOI":"10.1007\/3-540-60385-9_13"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"L. Yang, D. Gao, J. Mostoufi, R. Joshi, and P. Loewenstein. System design methodology of UltraSPARCTM-I. In 32nd Design Automation Conference, pages 7\u201312, 1995.","DOI":"10.1145\/217474.217481"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60385-9_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:01:56Z","timestamp":1742598116000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60385-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540603856","9783540455165"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-60385-9_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}