{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:37:08Z","timestamp":1725550628132},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540291053"},{"type":"electronic","value":"9783540320302"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11560548_24","type":"book-chapter","created":{"date-parts":[[2005,10,6]],"date-time":"2005-10-06T05:38:22Z","timestamp":1128577102000},"page":"317-331","source":"Crossref","is-referenced-by-count":10,"title":["Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification"],"prefix":"10.1007","author":[{"given":"Sudhindra","family":"Pandav","sequence":"first","affiliation":[]},{"given":"Konrad","family":"Slind","sequence":"additional","affiliation":[]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer Aided Verification","author":"J.R. Burch","year":"1994","unstructured":"Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 68\u201380. Springer, Heidelberg (1994)"},{"unstructured":"German, S.: Personal Communication","key":"24_CR2"},{"issue":"3-4","key":"24_CR3","first-page":"295","volume":"48","author":"T.J. Siegel","year":"2004","unstructured":"Siegel, T.J., Pfeffer, E., Magee, J.A.: The IBM eServer z990 microprocessor. IBM J. Res. Dev.\u00a048(3-4), 295\u2013309 (2004)","journal-title":"IBM J. Res. Dev."},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Computer Aided Verification","author":"R.E. Bryant","year":"2002","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: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 78\u201392. Springer, Heidelberg (2002)"},{"issue":"1","key":"24_CR5","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1109\/TSE.1975.6312821","volume":"1","author":"S. German","year":"1975","unstructured":"German, S., Wegbreit, B.: A synthesizer of inductive assertions. IEEE Trans. Software Eng.\u00a01(1), 68\u201375 (1975)","journal-title":"IEEE Trans. Software Eng."},{"key":"24_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal verification of reactive systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal verification of reactive systems: Safety. Springer, Heidelberg (1995)"},{"key":"24_CR7","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.\u00a02031, pp. 113\u2013127. Springer, Heidelberg (2001)"},{"issue":"1","key":"24_CR8","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0304-3975(96)00191-0","volume":"173","author":"N. Bjorner","year":"1997","unstructured":"Bjorner, N., Browne, A., Manna, Z.: Automatic generation of invariants and intermediate assertions. Theor. Comput. Sci.\u00a0173(1), 49\u201387 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/3-540-61474-5_80","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1996","unstructured":"Bensalem, S., Lakhnech, Y., Sa\u00efdi, H.: Powerful techniques for the automatic generation of invariants. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 323\u2013335. Springer, Heidelberg (1996)"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-540-36126-X_2","volume-title":"Formal Methods in Computer-Aided Design","author":"S. Das","year":"2002","unstructured":"Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 19\u201332. Springer, Heidelberg (2002)"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/3-540-47813-2_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K. Baukus","year":"2002","unstructured":"Baukus, K., Lakhnech, Y., Stahl, K.: Parameterized verification of a cache coherence protocol: Safety and liveness. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol.\u00a02294, pp. 317\u2013330. Springer, Heidelberg (2002)"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Computer Aided Verification","author":"S. Das","year":"1999","unstructured":"Das, S., Dill, D., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 160\u2013171. Springer, Heidelberg (1999)"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-27813-9_11","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2004","unstructured":"Lahiri, S.K., Bryant, R.: Indexed predicate discovery for unbounded system verification. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 135\u2013147. Springer, Heidelberg (2004)"},{"key":"24_CR14","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.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"key":"24_CR15","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1145\/237502.237573","volume-title":"SPAA 1996","author":"S. Park","year":"1996","unstructured":"Park, S., Dill, D.L.: Verification of flash cache coherence protocol by aggregation of distributed transactions. In: SPAA 1996, pp. 288\u2013296. ACM Press, New York (1996)"},{"key":"24_CR16","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":"P.K. Mannava","year":"2004","unstructured":"Mannava, P.K., Chou, C.T., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 382\u2013398. Springer, Heidelberg (2004)"},{"key":"24_CR17","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":"K. McMillan","year":"2001","unstructured":"McMillan, K.: Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, pp. 179\u2013195. Springer, Heidelberg (2001)"},{"key":"24_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-540-39724-3_22","volume-title":"Correct Hardware Design and Verification Methods","author":"E.A. Emerson","year":"2003","unstructured":"Emerson, E.A., Kahlon, V.: Exact and efficient verification of parameterized cache coherence protocols. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 247\u2013262. Springer, Heidelberg (2003)"},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-31980-1_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.D. Bingham","year":"2005","unstructured":"Bingham, J.D., Hu, A.J.: Empirically efficient verification for a class of infinite-state systems. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 77\u201392. Springer, Heidelberg (2005)"},{"unstructured":"Lahiri, S.: Personal Communication","key":"24_CR20"},{"unstructured":"Pandav, S., Slind, K., Gopalakrishnan, G.: Mutual exclusion property verification of FLASH cache coherence protocol. Technical Report UUCS-04-010, School of Computing, University of Utah (2004)","key":"24_CR21"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11560548_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:38:30Z","timestamp":1558273110000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560548_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291053","9783540320302"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/11560548_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}