{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:28:23Z","timestamp":1761596903679},"reference-count":13,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1995,3,1]],"date-time":"1995-03-01T00:00:00Z","timestamp":794016000000},"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":[[1995,3]]},"DOI":"10.1007\/bf01383968","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T09:32:59Z","timestamp":1112434379000},"page":"217-232","source":"Crossref","is-referenced-by-count":66,"title":["Verification of the Futurebus+ cache coherence protocol"],"prefix":"10.1007","volume":"6","author":[{"given":"Edmund M.","family":"Clarke","sequence":"first","affiliation":[]},{"given":"Orna","family":"Grumberg","sequence":"additional","affiliation":[]},{"given":"Hiromi","family":"Hiraishi","sequence":"additional","affiliation":[]},{"given":"Somesh","family":"Jha","sequence":"additional","affiliation":[]},{"given":"David E.","family":"Long","sequence":"additional","affiliation":[]},{"given":"Kenneth L.","family":"McMillan","sequence":"additional","affiliation":[]},{"given":"Linda A.","family":"Ness","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","unstructured":"R.E. Bryant, ?Graph-based algorithms for boolean function manipulation.?IEEE Transactions on Computers, C-35(8), 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, and D.E. Long, ?Representing circuits more efficiently in symbolic model checking.? InProceedings of the 28th ACM\/IEEE Design Automation Conference. IEEE Computer Society Press, June 1991.","DOI":"10.1145\/127601.127702"},{"key":"CR3","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.? InProceedings of the 27th ACM\/IEEE Design Automation Conference. ACM\/IEEE, IEEE Computer Society Press, June 1990.","DOI":"10.1145\/123186.123223"},{"key":"CR4","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D. L. Dill, and H. Hwang, ?Symbolic model checking: 1020 states and beyond.? InProceedings of the Fifth Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1990."},{"key":"CR5","unstructured":"E.M. Clarke and E.A. Emerson, ?Synthesis of synchronization skeletons for branching time temporal logic.? InLogic of Programs: Workshop, Yorktown, Heights, NY, May 1981, volume 131 ofLecture Notes in Computer Science. Springer-Verlag, 1981."},{"issue":"2","key":"CR6","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla, ?Automatic verification of finite-state concurrent systems using temporal logic specifications.?ACM Transactions on Programming Languages and Systems, 8(2):244?263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"CR7","unstructured":"P. Dixon, ?Multilevel cache architectures?. Minutes of the Futurebus+ Working Group meeting, December 1988."},{"key":"CR8","unstructured":"IEEE Computer Soceity.IEEE Standard for Futurebus+?Logical Protocol Specification, March 1992. IEEE Standard 896.1-1991."},{"key":"CR9","unstructured":"D.E. Long,Model Checking, Abstraction, and Compositional Verification. Ph.D. thesis, Carnegie Mellon University, 1993."},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"K.L. McMillan.Symbolic Model Checking: An Approach to the State Explosion Problem. Ph.D. thesis, Carnegie Mellon University, 1992.","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"CR11","unstructured":"K.L. McMillan and J. Schwalbe, ?Formal verification of the Encore Gigamax cache consistency protocol?. InProceedings of the 1991 International Symposium on Shared Memory Multiprocessors, April 1991."},{"key":"CR12","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"A. Pnueli, ?A temporal logic of concurrent programs.?Theoretical Computer Science, 13:45?60, 1981.","journal-title":"Theoretical Computer Science"},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"J.P. Quielle and J. Sifakis, ?Specification and verification of concurrent systems in CESAR?. InProceedings of the Fifth International Symposium in Programming, 1981.","DOI":"10.1007\/3-540-11494-7_22"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383968.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01383968\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383968","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T16:35:54Z","timestamp":1586190954000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01383968"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,3]]},"references-count":13,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1995,3]]}},"alternative-id":["BF01383968"],"URL":"https:\/\/doi.org\/10.1007\/bf01383968","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,3]]}}}