{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T03:55:39Z","timestamp":1791172539635,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540614746","type":"print"},{"value":"9783540685999","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61474-5_65","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:40:37Z","timestamp":1330292437000},"page":"147-158","source":"Crossref","is-referenced-by-count":25,"title":["Verifying systems with replicated components in mur\u03d5"],"prefix":"10.1007","author":[{"given":"C. Norris","family":"Ip","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K. R. Apt","year":"1986","unstructured":"Krzysztof R. Apt and Dexter C. Kozen. Limits for automatic verification of finitestate concurrent systems. Information Processing Letters, 22:307\u2013309, 1986.","journal-title":"Information Processing Letters"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, S. Bensalem, S. Graf. C. Loiseaux, and J. Sifakis. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 1993.","DOI":"10.1007\/3-540-56496-9_21"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"F. Balarin and A.L. Sangiovanni-Vincentelli. On the automatic computation of network invariants. 6th Int'l Conf. on Computer-Aided Verification, June 1994.","DOI":"10.1007\/3-540-58179-0_58"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. Abstract interpretation and application to logic programs. Technical report, Ecole Polytechnique, Laboratoire d'Informatique, 1992.","DOI":"10.1016\/0743-1066(92)90030-7"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"E.M. Clarke and O. Grumberg. Avoiding the state explosion problem in temporal logic model checking algorithms. Proceedings of the 6th Annual ACM Symp. on Priniciple of Distributed Computing, 1987.","DOI":"10.1145\/41840.41865"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and S. Jha. Verifying parameterized networks using abstraction and regular languages. CONCUR'95, 1995.","DOI":"10.1007\/3-540-60218-6_30"},{"key":"13_CR7","unstructured":"David L. Dill, Andreas J. Drexler, Alan J. Hu, and C. Han Yang. Protocol verification as a hardware design aid. Int'l Conf. on Computer Design: VLSI in Computers and Processors, 1992."},{"key":"13_CR8","unstructured":"E.J. Dijkstra. Invariance and nondeterminacy. In Mathematical Logic and Programming Languages. Prentice-Hall, 1985."},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. 5th Int'l Conf. on Computer-Aided Verification, April 1993.","DOI":"10.1007\/3-540-56922-7_7"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Susanne Graf. Verification of a distributed cache memory by using abstractions. 6th Int'l Conf. on Computer-Aided Verification, 1994.","DOI":"10.1007\/3-540-58179-0_55"},{"issue":"3","key":"13_CR11","doi-asserted-by":"crossref","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S.M. German","year":"1992","unstructured":"S.M. German and A.P. Sistla. Reasoning about systems with many processes. Journal of Association for Computing Machinery, 39(3):675\u2013735, 1992.","journal-title":"Journal of Association for Computing Machinery"},{"key":"13_CR12","unstructured":"C. Norris Ip and David L. Dill. Better verification through symmetry. 11th Int'l Symp. on Computer Hardware Description Languages and Their Applications, 1993. Extended version with complete proofs and semantic analysis to appear in Formal Methods in System Design."},{"key":"13_CR13","unstructured":"C. Norris Ip and David L. Dill. Efficient verification of symmetric concurrent systems. Int'l Conf. on Computer Design: VLSI in Computers and Processors, 1993."},{"key":"13_CR14","unstructured":"C. Norris Ip and David L. Dill. State reduction using reversible rules. 33rd Design Automation Conference, June 1996."},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Robert P. Kurshan, Michael Merritt, Ariel Orda, and Sonia R. Sachs. A structural linearization principle for processes. Formal Methods in System Design, 5, 1994.","DOI":"10.1007\/BF01383832"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Daniel Lenoski, James Laudon, Kourosh Gharachorloo, Anoop Gupta, and John Hennessy. The directory-based cache coherence protocol for the dash multiprocessor. 17th Int'l Symp. on Computer Architecture, 1990.","DOI":"10.1145\/325164.325132"},{"key":"13_CR17","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/BF00289237","volume":"21","author":"B. D. Lubachevsky","year":"1984","unstructured":"Boris D. Lubachevsky. An approach to automating the verification of compact parallel coordination programs I. Acta Informatica, 21:125\u2013169, 1984.","journal-title":"Acta Informatica"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"F. Pong and M. Dubois. Correctness of a directory-based cache coherence protocol: Early experience. 5th Symp. on Parallel Distributed Processing, 1993.","DOI":"10.1109\/SPDP.1993.395553"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"F. Pong and M. Dubois. A new approach for the verification of cache coherence protocols. IEEE Transactions on Parallel and Distributed Systems, 6(2), 1995.","DOI":"10.1109\/71.406955"},{"key":"13_CR20","unstructured":"F. Pong, A. Nowatzyk, G. Aybay, and M. Dubois. Verifying distributed directorybased cache coherence protocols: S3.mp, a case study. EurPar'95."},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Fong Pong. Symbolic State Model: A New Approach for the Verification of Cache Coherence Protocols. PhD thesis, University of Southern California, 1995.","DOI":"10.1109\/71.406955"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"June-Kyung Rho and Fabio Somenzi. Automatic generation of network invariants for the verification of iterative sequential systems. 5th Int'l Conf. on Computer-Aided Verification, June 1993.","DOI":"10.1007\/3-540-56922-7_11"},{"key":"13_CR23","unstructured":"A.P. Sistla and S.M. German. Reasoning with many processes. Symp. on Logic in Computer Science, 1987."},{"key":"13_CR24","unstructured":"Kenji Shibata, Yutaka Hirakawa, Akira Takura, and Tadashi Ohta. Reachability analysis for specified processes in a behavior description. IEICE Transaction on Communication, E76-B(11), November 1993."},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"Pierre Wolper and Vinciane Lovinfosse. Verifying properties of large sets of processes with network invariants. In Automatic Verification Methods for Finite State Systems, volume 407 of LNCS, Springer-Verlag, 1989.","DOI":"10.1007\/3-540-52148-8_6"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61474-5_65.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T10:36:04Z","timestamp":1640946964000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61474-5_65"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614746","9783540685999"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-61474-5_65","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}