{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T21:37:01Z","timestamp":1775684221543,"version":"3.50.1"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[1996,8,1]],"date-time":"1996-08-01T00:00:00Z","timestamp":838857600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1996,8]]},"DOI":"10.1007\/bf00625968","type":"journal-article","created":{"date-parts":[[2004,11,30]],"date-time":"2004-11-30T17:17:52Z","timestamp":1101835072000},"page":"41-75","source":"Crossref","is-referenced-by-count":169,"title":["Better verification through symmetry"],"prefix":"10.1007","volume":"9","author":[{"given":"C.","family":"Norris IP","sequence":"first","affiliation":[]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","first-page":"19","volume":"3","author":"S. Aggarwal","year":"1983","unstructured":"S. Aggarwal, R.P. Kurshan, and K. Sabnani, ?A calculus for protocol specification and validation,?Protocol Specification, Testing, and Verification, Vol. 3, pp. 19?34, 1983.","journal-title":"Protocol Specification, Testing, and Verification"},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, ?Symbolic model checking: 1020 states and beyond,?Proc. 5th Ann. IEEE Symp. on Logic in Computer Science, pp. 428?439, 1990.","DOI":"10.1109\/LICS.1990.113767"},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"K.M. Chandy and J. Misra,Parallel Program Design?A Foundation, Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"CR4","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 Transactions on Programming Languages and Systems, Vol. 8, No. 2, 1986.","DOI":"10.1145\/5397.5399"},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, T. Filkorn, and S. Jha, ?Exploiting symmetry in temporal logic model checking,?5th International Conference on Computer-Aided Verification, pp. 450?462, June 1993.","DOI":"10.1007\/3-540-56922-7_37"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"O. Coudert, C. Berthet, and J.C. Madre, ?Verification of synchronous sequential machines based on symbolic execution,?Automatic Verification Methods for Finite State Systems, pp. 365?373, 1989.","DOI":"10.1007\/3-540-52148-8_30"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"D.L. Dill, A.J. Drexler, A.J. Hu, and C.H. Yang, ?Protocol verification as a hardware design aid,?Proc. IEEE Int. Conf. on Computer Design: VLSI in Computers and Processors, pp. 522?525, 1992.","DOI":"10.1109\/ICCD.1992.276232"},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"C. Ebeling, ?GeminiII: A second generation layout validation program,?IEEE\/ACM Int. Conf. on Computer-Aided Design, pp. 322?325, 1988.","DOI":"10.21236\/ADA220731"},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and A.P. Sistla, ?Symmetry and model checking,?5th International Conference on Computer-Aided Verification, pp. 463?478, June 1993.","DOI":"10.1007\/3-540-56922-7_38"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"G.J. Holzmann,Automated Protocol Validation in Argos, Assertion Proving and Scatter Searching, Computer Science Press, pp. 163?188, 1987.","DOI":"10.1109\/TSE.1987.233206"},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"P. Huber, A.M. Jensen, L.O. Jepsen, and K. Jensen, ?Towards reachability trees for high-level Petri nets,?Advances on Petri Nets, pp. 215?233, 1984.","DOI":"10.1007\/3-540-15204-0_13"},{"key":"CR12","unstructured":"C.N. Ip and D.L. Dill, ?Better verification through symmetry,?Proc. 11th Int. Symp. on Computer Hardware Description Languages and Their Application, pp. 97?111, April 1993."},{"key":"CR13","unstructured":"C.N. Ip and D.L. Dill, ?Efficient verification of symmetric concurrent systems,?IEEE International Conference on Computer Design: VLSI in Computers and Processors, Cambridge, MA, pp. 230?234, October 3?6, 1993."},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"D. Lenoski, J. Laudon, K. Gharachorloo, A. Gupta, and J. Hennessy, ?The directory-based cache coherence protocol for the DASH multiprocessor,?Proc. 17th Int. Symp. on Computer Architercture, pp. 148?159, 1990.","DOI":"10.1145\/325096.325132"},{"issue":"No. 3","key":"CR15","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1109\/2.121510","volume":"25","author":"D. Lenoski","year":"1992","unstructured":"D. Lenoski, J. Laudon, K. Gharachorloo, W.-D. Weber, A. Gupta, J. Hennessy, M. Horowitz, and M. Lam, ?The Stanford DASH multiprocessor,?Computer, Vol. 25, No. 3, pp. 63?79, 1992.","journal-title":"Computer"},{"issue":"No. 2","key":"CR16","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/BF00289237","volume":"21","author":"B.D. Lubachevsky","year":"1984","unstructured":"B.D. Lubachevsky, ?An approach to automating the verification of compact parallel coordination programs, I,?Acta Informatica, Vol. 21, No. 2, pp. 125?169, 1984.","journal-title":"Acta Informatica"},{"issue":"No. 1","key":"CR17","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1145\/103727.103729","volume":"9","author":"J.M. Mellor-Crummey","year":"1991","unstructured":"J.M. Mellor-Crummey and M.L. Scott, ?Algorithms for scalable synchronization on shared-memory multiprocessors,?ACM Transactions on Computer Systems, Vol. 9, No. 1, pp. 21?65, 1991.","journal-title":"ACM Transactions on Computer Systems"},{"key":"CR18","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/0020-0190(88)90037-3","volume":"29","author":"H.B. Mittal","year":"1988","unstructured":"H.B. Mittal, ?A fast backtrack algorithm for graph isomorphism,?Information Processing Letters, Vol. 29, pp. 105?110, 1988.","journal-title":"Information Processing Letters"},{"issue":"No. 3","key":"CR19","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"G.L. Peterson","year":"1981","unstructured":"G.L.Peterson, ?Myths about the mutual exclusion problem,?Information Processing Letters, Vol. 12, No. 3, pp. 105?110, 1981.","journal-title":"Information Processing Letters"},{"issue":"No. 4\/5","key":"CR20","first-page":"293","volume":"8","author":"P.H. Starke","year":"1991","unstructured":"P.H. Starke, ?Reachability analysis of petri nets using symmetries,?Systems Analysis?Modelling?Simulation, Vol. 8, No. 4\/5, pp. 293?303, 1991.","journal-title":"Systems Analysis?Modelling?Simulation"},{"key":"CR21","doi-asserted-by":"crossref","unstructured":"H.J. Touati, H. Savoj, B. Lin, R.K. Brayton, and A. Sangiovanni-Vincentelli, ?Implicit state enumeration of finite state machines using BDDs,?IEEE Int. Conf. on Computer-Aided Design, pp. 130?133, 1990.","DOI":"10.1109\/ICCAD.1990.129860"},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"P. Wolper, ?Expressing interesting properties of programs,?13th Annual ACM Symp. on Principles of Programming Languages, 1986.","DOI":"10.1145\/512644.512661"},{"key":"CR23","doi-asserted-by":"crossref","unstructured":"P. Zafiropulo, C.H. West, H. Rudin, D.D. Cowan, and D. Brand, ?Towards analyzing and synthesizing protocols,?IEEE Transactions on Communications, Vol. COM-28, No. 4, 1980.","DOI":"10.1109\/TCOM.1980.1094687"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00625968.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00625968\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00625968","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,20]],"date-time":"2024-12-20T22:05:44Z","timestamp":1734732344000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00625968"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,8]]},"references-count":23,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1996,8]]}},"alternative-id":["BF00625968"],"URL":"https:\/\/doi.org\/10.1007\/bf00625968","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,8]]}}}