{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T18:11:18Z","timestamp":1649095878978},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2006,9,1]],"date-time":"2006-09-01T00:00:00Z","timestamp":1157068800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Comput Sci Technol"],"published-print":{"date-parts":[[2006,9]]},"DOI":"10.1007\/s11390-006-0765-6","type":"journal-article","created":{"date-parts":[[2006,10,15]],"date-time":"2006-10-15T06:38:59Z","timestamp":1160894339000},"page":"765-775","source":"Crossref","is-referenced-by-count":2,"title":["Model Checking Data Consistency for Cache Coherence Protocols"],"prefix":"10.1007","volume":"21","author":[{"given":"Hong","family":"Pan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hui-Min","family":"Lin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yi","family":"Lv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"765_CR1","doi-asserted-by":"crossref","unstructured":"Baukus K, Lakhnech Y, Stahl K. Parameterized verification of a cache coherence protocol: Safety and liveness. In Proc. VMCAI\u201902, Venice, Italy, LNCS 2294, Springer-Verlag, 2002, pp. 317\u2013330.","DOI":"10.1007\/3-540-47813-2_22"},{"key":"765_CR2","doi-asserted-by":"crossref","unstructured":"Chou C T, Mannava P K, Park S. A simple method for parameterized verification of cache coherence protocols. In FMCAD\u201904, Austin, Texas, USA, LNCS 3312, Springer-Verlag, 2004, pp. 382\u2013398.","DOI":"10.1007\/978-3-540-30494-4_27"},{"key":"765_CR3","doi-asserted-by":"crossref","unstructured":"Pnueli A, Ruah S, Zuck L. Automatic deductive verification with invisible invariants. In TACAS\u201901, Genova, Italy, LNCS 2031, Springer-Verlag, 2001, pp. 82\u201397.","DOI":"10.1007\/3-540-45319-9_7"},{"key":"765_CR4","doi-asserted-by":"crossref","unstructured":"Lahiri S K, Bryant R. Indexed predicate discovery for unbounded system verification. In CAV\u201904, Boston, Massachusetts, USA, LNCS 3114, Springer-Verlag, 2004, pp. 135\u2013147.","DOI":"10.1007\/978-3-540-27813-9_11"},{"key":"765_CR5","doi-asserted-by":"crossref","unstructured":"Emerson E A, Lahon V. Exact and efficient verification of parameterized cache coherence protocols. In CHARME\u201903, L\u2019Aquila, Italy, 2003, pp. 247\u2013262.","DOI":"10.1007\/978-3-540-39724-3_22"},{"key":"765_CR6","doi-asserted-by":"crossref","unstructured":"McMillan K. Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In CHARME\u201901, Livingston, Scotland, LNCS 2144, Springer-Verlag, 2001, pp. 179\u2013195.","DOI":"10.1007\/3-540-44798-9_17"},{"key":"765_CR7","doi-asserted-by":"crossref","unstructured":"McMillan K. Verification of infinite state systems by compositional model checking. In CHARME\u201999, Bad Herrenalb, Germany, LNCS 1703, Springer-Verlag, 1999, pp. 219\u2013233.","DOI":"10.1007\/3-540-48153-2_17"},{"key":"765_CR8","doi-asserted-by":"crossref","unstructured":"McMillan K, Qadeer S, Saxe J B. Induction in compositional model checking. In CAV\u201900, Chicago, IL, USA, LNCS 1855, 2000, pp. 312\u2013327.","DOI":"10.1007\/10722167_25"},{"key":"765_CR9","doi-asserted-by":"crossref","unstructured":"Emerson E A, Lahon V. Reducing model checking for the many to the few. In CADE\u201900, Pittsburgh, PA, USA, LNCS 1831, 2000, pp. 236\u2013254.","DOI":"10.1007\/10721959_19"},{"key":"765_CR10","doi-asserted-by":"crossref","unstructured":"Das S, Dill D, Park S. Experience with predicate abstraction. In CAV\u201999, Trento, Italy, LNCS 1633, Springer-Verlag, 1999, pp. 160\u2013171.","DOI":"10.1007\/3-540-48683-6_16"},{"key":"765_CR11","doi-asserted-by":"crossref","unstructured":"Graf S, Saidi H. Construction of abstract state graphs with PVS. In CAV\u201997, Haifa, Israel, LNCS 1254, Springer-Verlag, 1997, pp. 72\u201383.","DOI":"10.1007\/3-540-63166-6_10"},{"key":"765_CR12","doi-asserted-by":"crossref","unstructured":"Bryant R E, Lahiri S K, Seshia S A. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In CAV\u201902, Copenhagen, Denmark, LNCS 2404, Springer-Verlag, 2002, pp. 78\u201392.","DOI":"10.1007\/3-540-45657-0_7"},{"key":"765_CR13","doi-asserted-by":"crossref","unstructured":"Lahiri S K, Bryant R. Constructing quantified invariants via predicate abstraction. In VMCAI\u201904, Venice, Italy, LNCS 2937, Springer-Verlag, 2004, pp. 267\u2013281.","DOI":"10.1007\/978-3-540-24622-0_22"},{"key":"765_CR14","unstructured":"Lin H. Model checking value-passing processes. In APSEC\u20192001, Macau, December 4\u20137, IEEE Computer Society, 2001 pp. 3\u201310."},{"key":"765_CR15","doi-asserted-by":"crossref","unstructured":"Lin H. \u201cOn-the-fly\u201d instantiation of value-passing processes. In FORTE\/PSTV\u201998, Paris, France, Kluwer Academic Publishers, 1998, pp. 215\u2013230.","DOI":"10.1007\/978-0-387-35394-4_14"},{"key":"765_CR16","unstructured":"Milner R. Communication and Concurrency. Prentice-Hall, 1989."},{"key":"765_CR17","unstructured":"German S, Janssen G. Tutorial on verification of distributed cache memory protocols. In FMCAD\u201904, Austin, Texas, USA, 2004."}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-006-0765-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-006-0765-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-006-0765-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T10:32:37Z","timestamp":1559385157000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-006-0765-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,9]]},"references-count":17,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2006,9]]}},"alternative-id":["765"],"URL":"https:\/\/doi.org\/10.1007\/s11390-006-0765-6","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,9]]}}}