{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:19:01Z","timestamp":1755998341876},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319249520"},{"type":"electronic","value":"9783319249537"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24953-7_15","type":"book-chapter","created":{"date-parts":[[2015,10,7]],"date-time":"2015-10-07T11:00:11Z","timestamp":1444215611000},"page":"207-213","source":"Crossref","is-referenced-by-count":4,"title":["ParaVerifier: An Automatic Framework for Proving Parameterized Cache Coherence Protocols"],"prefix":"10.1007","author":[{"given":"Yongjian","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Pang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yi","family":"Lv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dongrui","family":"Fan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shen","family":"Cao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kaiqiang","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"0302","DOI":"10.1007\/3-540-61474-5_68","volume-title":"Computer Aided Verification","author":"A Pnueli","year":"1996","unstructured":"Pnueli, A., Shahar, E.: A platform for combining deductive with algorithmic verification. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 0302\u20139743. Springer, Heidelberg (1996)"},{"issue":"1","key":"15_CR2","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0304-3975(96)00191-0","volume":"173","author":"N Bj\u00f6rner","year":"1997","unstructured":"Bj\u00f6rner, N., Browne, A., Manna, Z.: Automatic generation of invariants and intermediate assertions. Theoret. Comput. Sci. 173(1), 49\u201387 (1997)","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 221\u2013234. Springer, Heidelberg (2001)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-45319-9_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Tiwari","year":"2001","unstructured":"Tiwari, A., Rue\u00df, H., Sa\u00efdi, H., Shankar, N.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 113\u2013127. Springer, Heidelberg (2001)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-30494-4_27","volume-title":"Formal Methods in Computer-Aided Design","author":"C-T Chou","year":"2004","unstructured":"Chou, C.-T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 382\u2013398. Springer, Heidelberg (2004)"},{"issue":"1","key":"15_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jlap.2006.08.007","volume":"71","author":"J Pang","year":"2007","unstructured":"Pang, J., Fokkink, W., Hofman, R., Veldema, R.: Model checking a cache coherence protocol of a java DSM implementation. J. Logic Algebraic Program. 71(1), 1\u201343 (2007)","journal-title":"J. Logic Algebraic Program."},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/11560548_24","volume-title":"Correct Hardware Design and Verification Methods","author":"S Pandav","year":"2005","unstructured":"Pandav, S., Slind, K., Gopalakrishnan, G.C.: Counterexample guided invariant discovery for parameterized cache coherence verification. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 317\u2013331. Springer, Heidelberg (2005)"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Lv, Y., Lin, H., Pan, H.: Computing invariants for parameter abstraction. In: Proceedings of the 5th IEEE\/ACM Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 29\u201338, IEEE CS (2007)","DOI":"10.1109\/MEMCOD.2007.371252"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Bingham B.: Automatic non-interference lemmas for parameterized model checking. In: Proceedings of the 8th Conference on Formal Methods in Computer-Aided Design (FMCAD), pp.1\u20138. IEEE CS (2008)","DOI":"10.1109\/FMCAD.2008.ECP.15"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"718","DOI":"10.1007\/978-3-642-31424-7_55","volume-title":"Computer Aided Verification","author":"S Conchon","year":"2012","unstructured":"Conchon, S., Goel, A., Krsti\u0107, S., Mebsout, A., Za\u00efdi, F.: Cubicle: a parallel smt-based model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 718\u2013724. Springer, Heidelberg (2012)"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/3-540-44798-9_17","volume-title":"Correct Hardware Design and Verification Methods","author":"KL McMillan","year":"2001","unstructured":"McMillan, K.L.: Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 179\u2013195. Springer, Heidelberg (2001)"},{"key":"15_CR13","series-title":"LNCS","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Park, S., Dill, D.L.: Verification of flash cache coherence protocol by aggregation of distributed transactions. In: Proceedings of the 8th Annual ACM Symposium on Parallel Algorithms and Architectures (SPAA), pp. 288\u2013296. ACM (1996)","DOI":"10.1145\/237502.237573"},{"key":"15_CR15","unstructured":"Li, Y.: invFinder: An invariant finder (2014). \n                    http:\/\/lcs.ios.ac.cn\/ lyj238\/invFinder.html"},{"key":"15_CR16","unstructured":"Technical Publications and Training, Intel Corporation: Forte\/FL User Guide (2003)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24953-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T00:07:29Z","timestamp":1559261249000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24953-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319249520","9783319249537"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24953-7_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}