{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T13:18:10Z","timestamp":1762521490713},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Supercomput"],"published-print":{"date-parts":[[2012,11]]},"DOI":"10.1007\/s11227-012-0755-0","type":"journal-article","created":{"date-parts":[[2012,4,16]],"date-time":"2012-04-16T09:30:52Z","timestamp":1334568652000},"page":"828-854","source":"Crossref","is-referenced-by-count":3,"title":["State space reduction in modeling checking parameterized cache coherence protocol by two-dimensional abstraction"],"prefix":"10.1007","volume":"62","author":[{"given":"Yang","family":"Guo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wanxia","family":"Qu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Long","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weixia","family":"Xu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,4,17]]},"reference":[{"key":"755_CR1","first-page":"231","volume-title":"Lecture notes in computing science","author":"O Grumberg","year":"2008","unstructured":"Grumberg O, Veith H (2008) 25 Years of model checking: history, achievements, perspectives. In: Lecture notes in computing science, vol\u00a05000, VII. Springer, Berlin, p 231"},{"issue":"3","key":"755_CR2","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/s00446-009-0092-6","volume":"22","author":"R Guerraoui","year":"2008","unstructured":"Guerraoui R, Henzinger TA, Singh V (2008) Model checking transactional memories. Distrib Comput 22(3):129\u2013145","journal-title":"Distrib Comput"},{"issue":"1","key":"755_CR3","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1145\/248621.248624","volume":"29","author":"F Pong","year":"1997","unstructured":"Pong F, Dubios M (1997) Verification techniques for cache coherence protocols. ACM Comput Surv 29(1):82\u2013126","journal-title":"ACM Comput Surv"},{"key":"755_CR4","volume-title":"The 27th annual int\u2019l symp on computer architecture (ISCA-2000)","author":"D Abts","year":"2000","unstructured":"Abts D, Lilja DJ, Scott S (2000) Toward complexity-effective verification: a case study of the cray SV2 cache coherence protocol. In: The 27th annual int\u2019l symp on computer architecture (ISCA-2000), Vancouver, British Columbia, Canada"},{"key":"755_CR5","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2008.12.027","volume":"223","author":"PA Abdulla","year":"2008","unstructured":"Abdulla PA, Delzanno G, Rezine A (2008) Monotonic abstraction in parameterized verification. Electron Notes Theor Comput Sci 223:3\u201314","journal-title":"Electron Notes Theor Comput Sci"},{"key":"755_CR6","doi-asserted-by":"crossref","unstructured":"Lahiri SK, Bryant RE (2007) Predicate abstraction with indexed predicates. ACM Trans Comput Logic 9(1). doi: 10.1145\/1297658.1297662","DOI":"10.1145\/1297658.1297662"},{"key":"755_CR7","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Proc of the 14th international conference on computer aided verification (CAV)","author":"A Pnueli","year":"2002","unstructured":"Pnueli A, Xu J, Zuck L (2002) Liveness with (0; 1; \u221e) counter abstraction. In: Proc of the 14th international conference on computer aided verification (CAV). Lecture notes in computer science, vol 2404. Springer, Berlin, pp 107\u2013122"},{"key":"755_CR8","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/11734666","volume-title":"Proc of the 7th VMCAI","author":"E Clarke","year":"2006","unstructured":"Clarke E, Talupur M, Veith H (2006) Environment abstraction for parameterized verification. In: Proc of the 7th VMCAI. Lecture notes in computer science, vol 3855. Springer, Berlin, pp 126\u2013141"},{"key":"755_CR9","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/978-3-540-78800-3_4","volume-title":"Proc of TACAS","author":"E Clarke","year":"2008","unstructured":"Clarke E, Talupur M, Veith H (2008) Proving Ptolemy right: environment abstraction principle for parameterized verification. In: Proc of TACAS. Lecture notes in computer science, vol 4963. Springer, Berlin, pp 33\u201347"},{"key":"755_CR10","first-page":"82","volume-title":"Proc of the 7th TACAS","author":"A Pnueli","year":"2001","unstructured":"Pnueli A, Ruah S, Zuck L (2001) Automatic deductive verification with invisible invariants. In: Proc of the 7th TACAS, pp 82\u201397"},{"key":"755_CR11","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Proc of the 9th int\u2019l conf on computer aided verification","author":"S Graf","year":"1997","unstructured":"Graf S, Saidi H (1997) Construction of abstract state graphs with PVS. In: Proc of the 9th int\u2019l conf on computer aided verification. Springer, Berlin, pp 72\u201383"},{"issue":"6","key":"755_CR12","doi-asserted-by":"crossref","first-page":"556","DOI":"10.1109\/TPDS.2002.1011412","volume":"13","author":"DJ Sorin","year":"2002","unstructured":"Sorin DJ, Plakal M, Condon AE, et al (2002) Specifying and verifying a broadcast and a multicast snooping cache coherence protocol. IEEE Trans Parallel Distrib Syst 13(6):556\u2013577","journal-title":"IEEE Trans Parallel Distrib Syst"},{"key":"755_CR13","first-page":"522","volume-title":"IEEE intl conference on computer design","author":"DL Dill","year":"1992","unstructured":"Dill DL, Drexler AJ, Hu AJ, Yang CH (1992) Protocol verification as a hardware design aid. In: IEEE intl conference on computer design, pp 522\u2013525"},{"key":"755_CR14","volume-title":"Specifying systems: the TLA+ language and tools for hardware and software engineers","author":"L Lamport","year":"2002","unstructured":"Lamport L (2002) Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley, Reading"},{"key":"755_CR15","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/3-540-44798-9_17","volume-title":"Proc on correct hardware design and verification methods (CHARME)","author":"KL McMillan","year":"2001","unstructured":"McMillan KL (2001) Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: Proc on correct hardware design and verification methods (CHARME). Lecture notes in computer science, vol 2144. Springer, Berlin, pp 179\u2013195"},{"key":"755_CR16","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"382","DOI":"10.1007\/978-3-540-30494-4_27","volume-title":"Proc on formal methods in computer-aided design (FMCAD)","author":"C-T Chou","year":"2004","unstructured":"Chou C-T, Mannava PK, Park S (2004) A simple method for parameterized verification of cache coherence protocols. In: Proc on formal methods in computer-aided design (FMCAD). Lecture notes in computer science, vol 3312. Springer, Berlin, pp 382\u2013398"},{"key":"755_CR17","first-page":"1534","volume-title":"Proc of the ACM symposium on applied computing (SAC)","author":"Y Li","year":"2007","unstructured":"Li Y (2007) Mechanized proofs for the parameter abstraction and guard strengthening principle in parameterized verification of cache coherence protocols. In: Proc of the ACM symposium on applied computing (SAC), pp 1534\u20131535"},{"issue":"1","key":"755_CR18","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/s10703-010-0092-y","volume":"36","author":"X Chen","year":"2010","unstructured":"Chen X, Yang Y, Gopalakrishnan G, Chou C-T (2010) Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols. Form Methods Syst Des 36(1):37\u201364","journal-title":"Form Methods Syst Des"},{"key":"755_CR19","volume-title":"Automated verification of infinite state systems (AVIS)","author":"S Krstic","year":"2005","unstructured":"Krstic S (2005) Parameterized system verification with guard strengthening and parameter abstraction. In: Automated verification of infinite state systems (AVIS)"},{"key":"755_CR20","volume-title":"Proc workshop on design of correct circuits (DCC)","author":"M Talupur","year":"2008","unstructured":"Talupur M, Krstic S, O\u2019Leary J, Tuttle MR (2008) Parametric verification of industrial strength cache coherence protocols. In: Proc workshop on design of correct circuits (DCC)"},{"key":"755_CR21","doi-asserted-by":"crossref","unstructured":"Talupur M, Tuttle M (2008) Going with the flow: parameterized verification using message flows. In: Formal methods in computer aided design (FMCAD), pp 1\u20138","DOI":"10.1109\/FMCAD.2008.ECP.14"},{"key":"755_CR22","first-page":"172","volume-title":"Proc of the 9th international conference on formal methods in computer-aided design (FMCAD)","author":"J O\u2019Leary","year":"2009","unstructured":"O\u2019Leary J, Talupur M, Tuttle MR (2009) Protocol verification using flows: an industrial experience. In: Proc of the 9th international conference on formal methods in computer-aided design (FMCAD), pp 172\u2013179"},{"key":"755_CR23","series-title":"Lecture notes in computer science","volume-title":"Proc of the 4th international conference on verification, model checking, and abstract interpretation","author":"A Pnueli","year":"2003","unstructured":"Pnueli A, Zuck LD (2003) Model-checking and abstraction to the aid of parameterized systems. In: Proc of the 4th international conference on verification, model checking, and abstract interpretation. Lecture notes in computer science, vol 2144. Springer, Berlin, p 4"},{"key":"755_CR24","volume-title":"Abstraction refinement for large scale model checking","author":"C Wang","year":"2006","unstructured":"Wang C, Hachtel GD, Somenzi F (2006) Abstraction refinement for large scale model checking. Springer, Berlin"},{"key":"755_CR25","first-page":"534","volume-title":"Lecture notes in computer science","author":"N Timm","year":"2010","unstructured":"Timm N, Wehrheim H (2010) On symmetries and spotlights\u2014verifying parameterised systems. In: Lecture notes in computer science, vol 6447. Springer, Berlin, pp 534\u2013548"},{"key":"755_CR26","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/978-3-540-45069-6_15","volume-title":"Proc of the international conference on computer-aided verification (CAV\u201903)","author":"SK Lahiri","year":"2003","unstructured":"Lahiri SK, Bryant RE, Cook B (2003) A symbolic approach to predicate abstraction. In: Proc of the international conference on computer-aided verification (CAV\u201903). Lecture notes in computer science, vol 2742. Springer, Berlin, pp 141\u2013153"},{"issue":"11","key":"755_CR27","doi-asserted-by":"crossref","first-page":"1144","DOI":"10.1016\/j.jsc.2008.11.006","volume":"45","author":"IV Konnov","year":"2010","unstructured":"Konnov IV, Zakharov VA (2010) An invariant-based approach to the verification of asynchronous parameterized networks. J Symb Comput 45(11):1144\u20131162","journal-title":"J Symb Comput"},{"key":"755_CR28","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/11560548_24","volume-title":"Proc of CHARME","author":"S Pandav","year":"2005","unstructured":"Pandav S, Slind L, Gopalakrishnan G (2005) Counterexample guided invariant discovery for parameterized cache coherence verification. In: Proc of CHARME. Lecture notes in computer science, vol 3725. Springer, Berlin, pp 317\u2013331"},{"key":"755_CR29","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"Proc of the 12th international conference on computer aided verification (CAV)","author":"G Delzanno","year":"2000","unstructured":"Delzanno G (2000) Automatic verification of parameterized of cache coherence protocols. In: Proc of the 12th international conference on computer aided verification (CAV), pp 53\u201368"},{"key":"755_CR30","first-page":"286","volume-title":"Proc of the 7th international conference on principles and practice of constraint programming","author":"G Delzanno","year":"2001","unstructured":"Delzanno G, Bultan T (2001) Constraint-based verification of client\u2013server protocols. In: Proc of the 7th international conference on principles and practice of constraint programming, pp 286\u2013301"},{"issue":"3","key":"755_CR31","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1023\/A:1026276129010","volume":"23","author":"G Delzanno","year":"2003","unstructured":"Delzanno G (2003) Constraint-based verification of parameterized cache coherence protocols. Form Methods Syst Des 23(3):257\u2013301","journal-title":"Form Methods Syst Des"},{"key":"755_CR32","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/978-3-540-39724-3_22","volume-title":"Proc on correct hardware design and verification methods (CHARME\u201903)","author":"EA Emerson","year":"2003","unstructured":"Emerson EA, Kahlon V (2003) Exact and efficient verification of parameterized cache coherence protocols. In: Proc on correct hardware design and verification methods (CHARME\u201903). Lecture notes in computer science, vol 2860. Springer, Berlin, pp 247\u2013262"},{"key":"755_CR33","series-title":"Lecture notes in computer science","first-page":"247","volume-title":"Proc VMCAI","author":"K Baukus","year":"2002","unstructured":"Baukus K, Lakhnech Y, Stahl K (2002) Parameterized verification of a cache coherence protocol: safety and liveness. In: Proc VMCAI. Lecture notes in computer science, vol 2294. Springer, Berlin, pp 247\u2013262"},{"key":"755_CR34","volume-title":"Model checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke EM Jr, Grumberg O, Peled DA (1999) Model checking. The MIT Press, Cambridge, London"},{"issue":"2","key":"755_CR35","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/s10626-007-0029-9","volume":"18","author":"A Girard","year":"2008","unstructured":"Girard A, Julius AA, Pappas GJ (2008) Approximate simulation relations for hybrid systems. Discret Event Dyn Syst 18(2):163\u2013179","journal-title":"Discret Event Dyn Syst"},{"key":"755_CR36","unstructured":"Talupur M (2006) Abstraction techniques for parameterized verification. Ph.D. Dissertation, Pittsburgh, Carnegie Mellon University"},{"key":"755_CR37","volume-title":"Parallel computer architecture: a hardware\/software approach","author":"D Culler","year":"1998","unstructured":"Culler D, Singh JP, Gupta A (1998) Parallel computer architecture: a hardware\/software approach. Morgan Kaufmann, San Mateo"},{"key":"755_CR38","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1023\/A:1026276129010","volume":"23","author":"G Delzanno","year":"2003","unstructured":"Delzanno G (2003) Constraint-based verification of parameterized cache coherence protocols. Form Methods Syst Des 23:257\u2013301","journal-title":"Form Methods Syst Des"},{"key":"755_CR39","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1007\/3-540-36577-X_11","volume-title":"Proc TACAS","author":"EA Emerson","year":"2003","unstructured":"Emerson EA, Kahlon V (2003) Rapid parameterized model checking of snoopy cache coherence protocols. In: Proc TACAS. Lecture notes in computer science, vol 2619. Springer, Berlin, pp 144\u2013159"},{"issue":"3","key":"755_CR40","doi-asserted-by":"crossref","first-page":"344","DOI":"10.1007\/s02011-011-1137-8","volume":"26","author":"X-J Yang","year":"2011","unstructured":"Yang X-J, Liao X-K, Lu K, et al (2011) The TianHe-1A supercomputer: its hardware and software. J\u00a0Comput Sci Technol 26(3):344\u2013351","journal-title":"J\u00a0Comput Sci Technol"},{"key":"755_CR41","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1007\/s11227-011-0593-5","volume":"58","author":"JL Bosque","year":"2011","unstructured":"Bosque JL, Roblas OD, Toharia P, Pastor L (2011) Evaluating scalability in heterogeneous systems. J\u00a0Supercomput 58:367\u2013375","journal-title":"J\u00a0Supercomput"}],"container-title":["The Journal of Supercomputing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/s11227-012-0755-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,27]],"date-time":"2019-06-27T10:24:17Z","timestamp":1561631057000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11227-012-0755-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,4,17]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,11]]}},"alternative-id":["755"],"URL":"https:\/\/doi.org\/10.1007\/s11227-012-0755-0","relation":{},"ISSN":["0920-8542","1573-0484"],"issn-type":[{"value":"0920-8542","type":"print"},{"value":"1573-0484","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,4,17]]}}}