{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T01:42:44Z","timestamp":1725500564266},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540775652"},{"type":"electronic","value":"9783540775669"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-77566-9_40","type":"book-chapter","created":{"date-parts":[[2008,1,5]],"date-time":"2008-01-05T06:18:43Z","timestamp":1199513923000},"page":"460-472","source":"Crossref","is-referenced-by-count":6,"title":["Verifying Parameterized taDOM+ Lock Managers"],"prefix":"10.1007","author":[{"given":"Antti","family":"Siirtola","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michal","family":"Valenta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"40_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining Liveness. Inf. Process. Lett.\u00a021, 181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"key":"40_CR2","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K.R. Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inform. Process. Lett.\u00a022, 307\u2013309 (1986)","journal-title":"Inform. Process. Lett."},{"key":"40_CR3","doi-asserted-by":"crossref","unstructured":"Attie, P.C., Emerson, E.A.: Synthesis of concurrent systems with many similar processes. ACM T. Progr. Lang. Sys., 51\u2013115 (1998)","DOI":"10.1145\/271510.271519"},{"key":"40_CR4","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"E.M. Clarke","year":"1996","unstructured":"Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Form. Method. Syst. Des.\u00a09, 77\u2013104 (1996)","journal-title":"Form. Method. Syst. Des."},{"key":"40_CR5","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"2001","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. MIT Press, Cambridge (2001)"},{"key":"40_CR6","unstructured":"Creese, S.J.: Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks. Ph.D. thesis, Oxford University (2001)"},{"key":"40_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/10721959_19","volume-title":"Automated Deduction - CADE-17","author":"E.A. Emerson","year":"2000","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) Automated Deduction - CADE-17. LNCS, vol.\u00a01831, pp. 236\u2013254. Springer, Heidelberg (2000)"},{"key":"40_CR8","doi-asserted-by":"crossref","unstructured":"Emerson, E. A., Kahlon, V.: Model checking guarded protocols. In: Proc. LICS 2003, Ottawa, pp. 361\u2013370 (2003)","DOI":"10.1109\/LICS.2003.1210076"},{"key":"40_CR9","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":"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":"40_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/978-3-540-30124-0_26","volume-title":"Computer Science Logic","author":"E.A. Emerson","year":"2004","unstructured":"Emerson, E.A., Kahlon, V.: Parameterized model checking of ring-based message passing systems. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 325\u2013339. Springer, Heidelberg (2004)"},{"key":"40_CR11","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Proc. POPL 1995, San Francisco, pp. 85\u201394 (1995)","DOI":"10.1145\/199448.199468"},{"key":"40_CR12","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"E.A. Emerson","year":"1996","unstructured":"Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Form. Method. Syst. Des.\u00a09, 105\u2013131 (1996)","journal-title":"Form. Method. Syst. Des."},{"key":"40_CR13","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, 675\u2013735 (1992)","journal-title":"J. ACM"},{"key":"40_CR14","unstructured":"Haustein, M., H\u00e4rder, T.: Optimizing concurrent XML processing. Internal report, Kaiserslautern University of Technology (2005), \n                    \n                      http:\/\/wwwlgis.informatik.uni-kl.de\/archiv\/wwwdvs.informatik.uni-kl.de\/pubs\/papers\/HH05.Int-Report.pdf"},{"key":"40_CR15","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1016\/j.datak.2006.06.015","volume":"61","author":"M. Haustein","year":"2007","unstructured":"Haustein, M., H\u00e4rder, T.: An efficient infrastructure for native transactional XML processing. Data Knowl. Eng.\u00a061, 500\u2013523 (2007)","journal-title":"Data Knowl. Eng."},{"key":"40_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/3-540-48683-6_27","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"1999","unstructured":"Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Verifying sequential consistency on shared-memory multiprocessor systems. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 301\u2013315. Springer, Heidelberg (1999)"},{"key":"40_CR17","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/BF00625968","volume":"9","author":"N. Ip","year":"1996","unstructured":"Ip, N., Dill, D.: Better verification through symmetry. Form. Method. Syst. Des.\u00a09, 41\u201375 (1996)","journal-title":"Form. Method. Syst. Des."},{"key":"40_CR18","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1023\/A:1008723125149","volume":"14","author":"N. Ip","year":"1999","unstructured":"Ip, N., Dill, D.: Verifying systems with replicated components in Mur\u03d5. Form. Method. Syst. Des.\u00a014, 273\u2013310 (1999)","journal-title":"Form. Method. Syst. Des."},{"key":"40_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1995.1024","volume":"117","author":"R.P. Kurshan","year":"1995","unstructured":"Kurshan, R.P., McMillan, K.: A structural induction theorem for processes. Inf. Comp.\u00a0117, 1\u201311 (1995)","journal-title":"Inf. Comp."},{"key":"40_CR20","unstructured":"Lazi\u0107, R.S.: A Semantic Study of Data Independence with Applications to Model Checking. Ph.D. thesis. Oxford University (2001)"},{"key":"40_CR21","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1109\/32.265633","volume":"20","author":"J. Li","year":"1994","unstructured":"Li, J., Suzuki, I., Yamashita, M.: A new structural induction theorem for rings of temporal Petri nets. IEEE T. Software Eng.\u00a020, 115\u2013126 (1994)","journal-title":"IEEE T. Software Eng."},{"key":"40_CR22","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/S0304-3975(00)00104-3","volume":"256","author":"D. Lesens","year":"2001","unstructured":"Lesens, D., Halbwachs, N., Raymond, P.: Automatic verification of parameterized networks of processes. Theor. Comput. Sci.\u00a0256, 113\u2013144 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"40_CR23","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/BF00289237","volume":"21","author":"B.D. Lubachevsky","year":"1984","unstructured":"Lubachevsky, B.D.: An approach to automating the verifcation of compact parallel coordination programs I. Acta Inform.\u00a021, 125\u2013169 (1984)","journal-title":"Acta Inform."},{"key":"40_CR24","unstructured":"Pyssysalo, T.: An Induction Theorem for Ring Protocols of Processes Described with Predicate\/Transition Nets. Research Reports, Helsinki University of Technology A37 (1996)"},{"key":"40_CR25","volume-title":"Database Management Systems","author":"R. Ramakrishnan","year":"2002","unstructured":"Ramakrishnan, R., Gehrke, J.: Database Management Systems, 3rd edn. McGraw Hill, New York (2002)","edition":"3"},{"key":"40_CR26","volume-title":"The Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1997","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, Englewood Cliffs (1997)"},{"key":"40_CR27","unstructured":"World Wide Web Consortium, \n                    \n                      http:\/\/www.w3c.org\/"},{"key":"40_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-52148-8_6","volume-title":"Automatic Verification Methods for Finite State Systems","author":"P. Wolper","year":"1990","unstructured":"Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol.\u00a0407, pp. 68\u201380. Springer, Heidelberg (1990)"},{"key":"40_CR29","unstructured":"Appendix, \n                    \n                      http:\/\/www.tol.oulu.fi\/~santti\/papers\/tadom_appendix.pdf"}],"container-title":["Lecture Notes in Computer Science","SOFSEM 2008: Theory and Practice of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-77566-9_40.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:45:01Z","timestamp":1619520301000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-77566-9_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540775652","9783540775669"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-77566-9_40","relation":{},"subject":[]}}