{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:51:20Z","timestamp":1725573080790},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540242970"},{"type":"electronic","value":"9783540305798"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-30579-8_9","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T16:45:34Z","timestamp":1292863534000},"page":"130-145","source":"Crossref","is-referenced-by-count":7,"title":["Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement"],"prefix":"10.1007","author":[{"given":"Sebastian","family":"Burckhardt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajeev","family":"Alur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Milo M. K.","family":"Martin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"9_CR1","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M. Abadi","year":"1995","unstructured":"Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages and Systems\u00a017(3), 507\u2013535 (1995)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"9_CR2","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1109\/LICS.1996.561320","volume-title":"Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science","author":"R. Alur","year":"1996","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p. 207. IEEE Computer Society, Los Alamitos (1996)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-44585-4_15","volume-title":"Computer Aided Verification","author":"R. Alur","year":"2001","unstructured":"Alur, R., Wang, B.: Verifying network protocol implementations by symbolic refinement checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 169. Springer, Heidelberg (2001)"},{"key":"9_CR4","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.\u00a02102, pp. 221\u2013234. Springer, Heidelberg (2001)"},{"issue":"3","key":"9_CR5","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1109\/40.768501","volume":"19","author":"Arvind","year":"1999","unstructured":"Arvind, Shen, X.: Using term rewriting systems to design and verify processors. IEEE Micro\u00a019(3), 36\u201346 (1999)","journal-title":"IEEE Micro"},{"issue":"1","key":"9_CR6","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90185-I","volume":"96","author":"G. Berry","year":"1992","unstructured":"Berry, G., Boudol, G.: The chemical abstract machine. Theoretical Computer Science\u00a096(1), 217\u2013248 (1992)","journal-title":"Theoretical Computer Science"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., et al.: Verifying safety of a token coherence implementation by parametric compositional refinement: Extended version (2004), http:\/\/www.seas.upenn.edu\/~sburckha\/token\/","DOI":"10.1007\/978-3-540-30579-8_9"},{"key":"9_CR8","unstructured":"Chandy, K.M., Misra, J.: Parallel program design: a foundation. Addison-Wesley Longman Publishing Co., Inc., Amsterdam (1988)"},{"issue":"5","key":"9_CR9","doi-asserted-by":"publisher","first-page":"726","DOI":"10.1145\/265943.265960","volume":"19","author":"E.M. Clarke","year":"1997","unstructured":"Clarke, E.M., Grumberg, O., Jha, S.: Verifying parameterized networks. ACM Trans. Program. Lang. Syst.\u00a019(5), 726\u2013750 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"Computer Aided Verification","author":"G. Delzanno","year":"2000","unstructured":"Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 53\u201368. Springer, Heidelberg (2000)"},{"key":"9_CR11","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/3-540-61474-5_86","volume-title":"Proceedings of the 8th International Conference on Computer Aided Verification","author":"D.L. Dill","year":"1996","unstructured":"Dill, D.L.: The murphi verification system. In: Proceedings of the 8th International Conference on Computer Aided Verification, pp. 390\u2013393. Springer, Heidelberg (1996)"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: International Conference on Computer Design, pp. 522\u2013525 (1992)","DOI":"10.1109\/ICCD.1992.276232"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: Conference on Automated Deduction, pp. 236\u2013254 (2000)","DOI":"10.1007\/10721959_19"},{"issue":"2","key":"9_CR14","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1023\/A:1022921522163","volume":"22","author":"S.M. German","year":"2003","unstructured":"German, S.M.: Formal design of cache memory protocols in IBM. Formal Methods in System Design\u00a022(2), 133\u2013141 (2003)","journal-title":"Formal Methods in System Design"},{"issue":"3","key":"9_CR15","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S.M. German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM\u00a039(3), 675\u2013735 (1992)","journal-title":"J. ACM"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: Algorithms for automated protocol verification. AT&T Tech. J. (January\/February 1990)","DOI":"10.1002\/j.1538-7305.1990.tb00101.x"},{"issue":"4","key":"9_CR17","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/s100090050040","volume":"2","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Control and data abstraction: The cornerstones of practical formal verification. International Journal on Software Tools for Technology Transfer\u00a02(4), 328\u2013342 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"9_CR18","volume-title":"Computer-aided verification of coordinating processes: the automata-theoretic approach","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press, Princeton (1994)"},{"key":"9_CR19","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1145\/72981.72998","volume-title":"Proceedings of the Eighth Annual ACM Symposium on Principles of Distributed Computing","author":"R.P. Kurshan","year":"1989","unstructured":"Kurshan, R.P., McMillan, K.: A structural induction theorem for processes. In: Proceedings of the Eighth Annual ACM Symposium on Principles of Distributed Computing, pp. 239\u2013247. ACM Press, New York (1989)"},{"key":"9_CR20","unstructured":"Martin, M.M.K.: Token Coherence. PhD thesis, University of Wisconsin-Madison (2003)"},{"key":"9_CR21","unstructured":"Martin, M.M.K., et al.: Protocol specifications and tables for four comparable MOESI coherence protocols: Token coherence, directory, snooping, and hammer (2003), http:\/\/www.cs.wisc.edu\/multifacet\/theses\/milo_martin_phd\/"},{"key":"9_CR22","first-page":"182","volume-title":"Proceedings of the 30th Annual International Symposium on Computer Architecture","author":"M.M.K. Martin","year":"2003","unstructured":"Martin, M.M.K., Hill, M.D., Wood, D.A.: Token coherence: decoupling performance and correctness. In: Proceedings of the 30th Annual International Symposium on Computer Architecture, pp. 182\u2013193. ACM Press, New York (2003)"},{"key":"9_CR23","unstructured":"McMillan, K., Schwalbe, J.: Formal verification of the Encore Gigamax cache consistency protocol. In: Proceedings of the International Symposium on Shared Memory Multiprocessing, Tokyo, Japan, pp. 242\u2013251 (1991)"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/3-540-63166-6_6","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"1997","unstructured":"McMillan, K.L.: A compositional rule for hardware design refinement. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 24\u201335. Springer, Heidelberg (1997)"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/BFb0028738","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"1998","unstructured":"McMillan, K.L.: Verification of an implementation of tomasulo\u2019s algorithm by compositional model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol.\u00a01427, pp. 110\u2013121. Springer, Heidelberg (1998)"},{"key":"9_CR26","volume-title":"Communicating and Mobile Systems: the \u03c0-Calculus","author":"R. Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile Systems: the \u03c0-Calculus. Cambridge University Press, Cambridge (1999)"},{"key":"9_CR27","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1145\/237502.237573","volume-title":"Proceedings of the Eighth Annual ACM Symposium on Parallel Algorithms and Architectures","author":"S. Park","year":"1996","unstructured":"Park, S., Dill, D.L.: Verification of FLASH cache coherence protocol by aggregation of distributed transactions. In: Proceedings of the Eighth Annual ACM Symposium on Parallel Algorithms and Architectures, pp. 288\u2013296. ACM Press, New York (1996)"},{"issue":"1","key":"9_CR28","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/248621.248624","volume":"29","author":"F. Pong","year":"1997","unstructured":"Pong, F., Dubois, M.: Verification techniques for cache coherence protocols. ACM Computing Surveys\u00a029(1), 82\u2013126 (1997)","journal-title":"ACM Computing Surveys"},{"key":"9_CR29","volume-title":"Handbook of Process Algebra","author":"A. Ponse","year":"2001","unstructured":"Ponse, A., Smolka, S.A., Bergstra, J.A.: Handbook of Process Algebra. Elsevier Science Inc., Amsterdam (2001)"},{"issue":"6","key":"9_CR30","doi-asserted-by":"publisher","first-page":"556","DOI":"10.1109\/TPDS.2002.1011412","volume":"13","author":"D.J. Sorin","year":"2002","unstructured":"Sorin, D.J., Plakal, M., Condon, A.E., Hill, M.D., Martin, M.M.K., Wood, D.A.: Specifying and verifying a broadcast and a multicast snooping cache coherence protocol. IEEE Transactions on Parallel and Distributed Systems\u00a013(6), 556\u2013578 (2002)","journal-title":"IEEE Transactions on Parallel and Distributed Systems"},{"key":"9_CR31","first-page":"414","volume-title":"Proceedings of the 13th Annual International Symposium on Computer Architecture","author":"P. Sweazey","year":"1986","unstructured":"Sweazey, P., Smith, A.J.: A class of compatible cache consistency protocols and their support by the IEEE futurebus. In: Proceedings of the 13th Annual International Symposium on Computer Architecture, pp. 414\u2013423. IEEE Computer Society Press, Los Alamitos (1986)"},{"key":"9_CR32","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1145\/512644.512661","volume-title":"Proceedings of the 13th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages","author":"P. Wolper","year":"1986","unstructured":"Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. In: Proceedings of the 13th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 184\u2013193. ACM Press, New York (1986)"},{"issue":"4","key":"9_CR33","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1109\/54.57906","volume":"7","author":"D.A. Wood","year":"1990","unstructured":"Wood, D.A., Gibson, G.A., Katz, R.H.: Verifying a multiprocessor cache controller using random test generation. IEEE Design & Test\u00a07(4), 13\u201325 (1990)","journal-title":"IEEE Design & Test"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30579-8_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:24:21Z","timestamp":1605759861000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30579-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540242970","9783540305798"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30579-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}