{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:40:32Z","timestamp":1725550832972},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008989"},{"type":"electronic","value":"9783540365778"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_23","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"315-330","source":"Crossref","is-referenced-by-count":6,"title":["Compositional Analysis for Verification of Parameterized Systems"],"prefix":"10.1007","author":[{"given":"Samik","family":"Basu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C. R.","family":"Ramakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"J. Archibald and J.L. Baer. Cache coherence protocols: Evaluation using a multi-processor simulation model. In ACM TOCS, 1986.","DOI":"10.1145\/6513.6514"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"O. Agesen, D. Detlefs, A. Garthwaite, R. Knippel, Y.S. Ramakrishna, and D. White. An efficient meta-lock for ubiquitous synchronization. In OOPSLA, 1999.","DOI":"10.1145\/320384.320402"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur and T. Henzinger. Reactive modules. In LICS, 1996.","DOI":"10.1109\/LICS.1996.561320"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"H. R. Andersen. Partial model checking. In LICS, 1995.","DOI":"10.1109\/LICS.1995.523274"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"H. R. Andersen, C. Stirling, and G. Winskel. A compositional proof system for the modal mu-calculus. In LICS, 1994.","DOI":"10.7146\/brics.v1i34.21609"},{"key":"23_CR6","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In LICS, 1990."},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"S. Berezin and D. Gurov. A compositional proof system for the modal mu-calculus and CCS. Technical Report CMU-CS-97-105, CMU, 1997.","DOI":"10.21236\/ADA342066"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"J. Bradfield and C. Stirling. Modal logics and mu-calculi: an introduction. In Handbook of Process Algebra. Elsevier, 2001.","DOI":"10.1016\/B978-044482830-9\/50022-9"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"S. Basu, S. A. Smolka, and O. R. Ward. Model checking the Java Meta-Locking algorithm. In ECBS, 2000.","DOI":"10.1109\/ECBS.2000.839894"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, 1977.","DOI":"10.1145\/512950.512973"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS, 1986.","DOI":"10.1145\/5397.5399"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and S. Jha. Verifying parameterized networks. In ACM transactions on programming languages and systems, 1997.","DOI":"10.1145\/265943.265960"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"R. Cleaveland and B. Steffen. A linear-time model checking algorithm for the alternation-free modal mu-calculus. FMSD, 1993.","DOI":"10.1007\/3-540-55179-4_6"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"G. Delzanno. Automatic verification of parameterized cache coherence protocols. In CAV, 2000.","DOI":"10.1007\/10722167_8"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"G. Delzanno and A. Podelski. Model checking in CLP. In TACAS, 1999.","DOI":"10.1007\/3-540-49059-0_16"},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"J. Esparza, A. Finkel, and R. Mayr. On the verification of broadcast protocols. In LICS, 1999.","DOI":"10.1109\/LICS.1999.782630"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and C. S. Jutla. The complexity of tree automata and logics of programs. In FOCS, pages 328\u2013337, 1988.","DOI":"10.1109\/SFCS.1988.21949"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and K.S. Namjoshi. Reasoning about rings. In POPL, 1995.","DOI":"10.1145\/199448.199468"},{"key":"23_CR19","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and K.S. Namjoshi. Automated verification of parameterized synchronous systems. In CAV, 1996.","DOI":"10.1007\/3-540-61474-5_60"},{"key":"23_CR20","unstructured":"E.A. Emerson and K.S. Namjoshi. On model checking for nondeterministic infinite state systems. In LICS, 1998."},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"O. Grumberg and D.E. Long. Model checking and modular verification. In TOPLAS, 1994.","DOI":"10.1145\/177492.177725"},{"key":"23_CR22","doi-asserted-by":"crossref","unstructured":"P. Van Hentenryck, A. Cortesi, and B. Le Charlier. Type analysis of prolog using type graphs. In JLP, 1994.","DOI":"10.1145\/178243.178479"},{"key":"23_CR23","doi-asserted-by":"crossref","unstructured":"G. J. Holzmann. The model checker SPIN. IEEE TSE, 1997.","DOI":"10.1109\/32.588521"},{"key":"23_CR24","unstructured":"T. Henzinger, S. Qadeer, and S.K. Rajamani. You assume, we guarantee. In CAV, 1998."},{"key":"23_CR25","unstructured":"C. N. Ip and D. L. Dill. Better verification through symmetry reduction. In FMSD, 1996."},{"key":"23_CR26","unstructured":"C.N. Ip and D.L. Dill. Verifying systems with replicated components in murphi. In FMSD, 1999."},{"key":"23_CR27","doi-asserted-by":"crossref","unstructured":"D. Kozen. Results on the propositional \u03bc-calculus. TCS, 1983.","DOI":"10.7146\/dpb.v11i146.7420"},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"Y. Kesten and A. Pnueli. Control and data abstraction:the cornerstones of pratical formal verification. In Intl. Journal on STTT, 2000.","DOI":"10.1007\/s100090050040"},{"key":"23_CR29","doi-asserted-by":"crossref","unstructured":"D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of linear networks processes. In POPL, 1997.","DOI":"10.1145\/263699.263747"},{"key":"23_CR30","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Compositional rule for hardware design refinement. In CAV, 1997.","DOI":"10.1007\/3-540-63166-6_6"},{"key":"23_CR31","unstructured":"R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989."},{"key":"23_CR32","unstructured":"P. Mildner. Type Domains form Abstract interpretation: A critical study.PhD thesis, Uppsala University, 1999."},{"key":"23_CR33","doi-asserted-by":"crossref","unstructured":"A. Pnueli and E. Shahar. Liveness and acceleration in parameterized verification. In CAV, 2000.","DOI":"10.1007\/10722167_26"},{"key":"23_CR34","doi-asserted-by":"crossref","unstructured":"J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proceedings of the International Symposium in Programming, 1982.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"23_CR35","doi-asserted-by":"crossref","unstructured":"A. Roychoudhury, K.N. Kumar, C.R. Ramakrishnan, I.V. Ramakrishnan, and S.A. Smolka. Verification of parameterized systems using logicprogram transformations. In TACAS, 2000.","DOI":"10.1007\/3-540-46419-0_13"},{"key":"23_CR36","doi-asserted-by":"crossref","unstructured":"A. Roychoudhury and I.V. Ramakrishnan. Automated inductive verification of parameterized protocols. In CAV, 2001.","DOI":"10.1007\/3-540-44585-4_4"},{"key":"23_CR37","unstructured":"A. P. Sistla and V. Gyuris. Parameterized verification of linear networks using automata as invariants. Formal Aspects of Computing, 1999."},{"key":"23_CR38","doi-asserted-by":"crossref","unstructured":"P. Wolper. Expressing interesting properties in propositional temporal logic. In POPL, 1986.","DOI":"10.1145\/512644.512661"},{"key":"23_CR39","unstructured":"The XSB Group. The XSB logic programming system v2.1, 2000. Available from http:\/\/www.cs.sunysb.edu\/~sbprolog ."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T18:45:44Z","timestamp":1558982744000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_23","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}