{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T04:59:33Z","timestamp":1773723573874,"version":"3.50.1"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2019,4,1]],"date-time":"2019-04-01T00:00:00Z","timestamp":1554076800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000769","name":"University of Oxford","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000769","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2019,10]]},"DOI":"10.1007\/s10009-019-00516-4","type":"journal-article","created":{"date-parts":[[2019,4,5]],"date-time":"2019-04-05T12:38:50Z","timestamp":1554467930000},"page":"567-605","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Symmetry reduction in CSP model checking"],"prefix":"10.1007","volume":"21","author":[{"given":"Thomas","family":"Gibson-Robinson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gavin","family":"Lowe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,4,1]]},"reference":[{"key":"516_CR1","first-page":"1447","volume-title":"Handbook of Combinatorics, , chapter\u00a027","author":"L Babai","year":"1995","unstructured":"Babai, L.: Automorphism groups, isomorphism, reconstruction. In: Graham, R.L., Gr\u00f6tschel, M., Lov\u00e1z, L. (eds.) Handbook of Combinatorics, chapter\u00a027, vol. II, pp. 1447\u20131540. North Holland, Amsterdam (1995)"},{"key":"516_CR2","doi-asserted-by":"crossref","unstructured":"Babai, L., Ku\u010dera, L.: Canonical labelling of graphs in linear average time. In: Proceedings of the 20th IEEE Symposium on Foundations of Computer Science, pp. 39\u201346 (1979)","DOI":"10.1109\/SFCS.1979.8"},{"key":"516_CR3","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/s100090200074","volume":"4","author":"D Bo\u0161na\u010dki","year":"2002","unstructured":"Bo\u0161na\u010dki, D., Dams, D., Holenderski, L.: Symmetric Spin. Int. J. Softw. Tools Technol. Transf. 4, 92\u2013106 (2002)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"516_CR4","unstructured":"Chen, K.: Analysing concurrent datatypes in CSP. Master\u2019s thesis, University of Oxford (2015)"},{"key":"516_CR5","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0304-3975(96)00010-2","volume":"176","author":"G Chiola","year":"1997","unstructured":"Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: A symbolic reachability graph for coloured petri nets. Theor. Comput. Sci. 176, 39\u201365 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"516_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Proceedings of the 10th International Conference on Computer-Aided Verification (CAV\u00a0\u201998), pp 147\u2013158 (1998)","DOI":"10.1007\/BFb0028741"},{"key":"516_CR7","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"EM Clarke","year":"1996","unstructured":"Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Form. Methods Syst. Design 9, 77\u2013104 (1996)","journal-title":"Form. Methods Syst. Design"},{"key":"516_CR8","doi-asserted-by":"crossref","unstructured":"Colvin, R., Groves, L.: Formal verification of an array-based nonblocking queue. In: Proceedings of 10th IEEE International Conference on Engineering of Complex Computer Systems, pp. 507\u2013516 (2005)","DOI":"10.1109\/ICECCS.2005.49"},{"key":"516_CR9","unstructured":"Donaldson, A.F., Miller, A.: A computational group theoretic symmetry reduction package for the spin model checker. In: 11th International Conference on Algebraic Methodology and Software Technology, AMAST 2006, Kuressaare, Estonia, July 5\u20138, 2006, Proceedings, pp. 374\u2013380 (2006)"},{"key":"516_CR10","doi-asserted-by":"crossref","unstructured":"Donaldson, A.F., Miller, A.: Extending symmetry reduction techniques to a realistic model of computation. Electronic Notes Theor. Comput. Sci. 185, 63\u201376 (2007) Proceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS 2006)","DOI":"10.1016\/j.entcs.2007.05.029"},{"key":"516_CR11","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Sistla, A.P.: Symmetry and model checking. In: Proceedings of 5th International Conference on Computer Aided Verification (1993)","DOI":"10.1007\/3-540-56922-7_38"},{"key":"516_CR12","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"EA Emerson","year":"1996","unstructured":"Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Form. Methods Syst. Design 9, 105\u2013131 (1996)","journal-title":"Form. Methods Syst. Design"},{"key":"516_CR13","doi-asserted-by":"crossref","unstructured":"Fischer, C., Wehrheim, H.: Model-checking CSP-OZ specifications with FDR. In: Proceedings of Integrated Formal Methods (IFM\u201999), pp. 315\u2013334 (1999)","DOI":"10.1007\/978-1-4471-0851-1_17"},{"key":"516_CR14","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/s10009-015-0377-y","volume":"18","author":"T Gibson-Robinson","year":"2015","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3: a parallel refinement checker for CSP. Int. J. Softw. Tools Technol. Transf. 18, 149\u2013167 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"516_CR15","unstructured":"Gibson-Robinson, T., Lowe, G.: Symmetry reduction in CSP model checking. Technical report, University of Oxford, Oxford (2015). \n                    http:\/\/www.cs.ox.ac.uk\/people\/gavin.lowe\/SymmetryReduction\/"},{"key":"516_CR16","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming, revised 1st edn. Morgan Kaufmann, Burlington (2012)"},{"issue":"3","key":"516_CR17","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"516_CR18","unstructured":"Iosif, R.: Exploiting heap symmetries in explicit-state model checking of software. In: 16th IEEE International Conference on Automated Software Engineering (ASE 2001), 26\u201329 November 2001, Coronado Island, San Diego, CA, pp 254\u2013261 (2001)"},{"key":"516_CR19","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/BF00625968","volume":"9","author":"CN Ip","year":"1996","unstructured":"Ip, C.N., Dill, D.L.: Better verification through symmetry. Form. Methods Syst. Design 9, 41\u201375 (1996)","journal-title":"Form. Methods Syst. Design"},{"key":"516_CR20","unstructured":"Janssen, R.: Verification of Concurrent Datatypes Using CSP. Master\u2019s thesis, University of Oxford (2015)"},{"key":"516_CR21","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/BF00625967","volume":"9","author":"K Jensen","year":"1996","unstructured":"Jensen, K.: Condensed state spaces for symmetrical coloured petri nets. Form. Methods Syst. Design 9, 7\u201340 (1996)","journal-title":"Form. Methods Syst. Design"},{"issue":"4","key":"516_CR22","first-page":"307","volume":"7","author":"TA Junttila","year":"2001","unstructured":"Junttila, T.A.: Computational complexity of the place\/transition-net symmetry reduction method. J. Univ. Comput. Sci. 7(4), 307\u2013326 (2001)","journal-title":"J. Univ. Comput. Sci."},{"key":"516_CR23","unstructured":"Junttila, T.A.: New orbit algorithms for data symmetries. In: Proceedings of the Fourth International Conference on Application of Concurrency to System Design (ACSD\u201904) (2004)"},{"key":"516_CR24","doi-asserted-by":"crossref","unstructured":"Lawrence, J.: Practical applications of CSP and FDR to software design. In: Communicating Sequential Processes: The First 25 Years, volume 3525 of Lecture Notes in Computer Science, pp. 151\u2013174. Springer, New York (2005)","DOI":"10.1007\/11423348_9"},{"key":"516_CR25","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Butler, M., Spermann, C., Turner, E.: Symmetry reduction for B by permutation flooding. In: Proceedings of 7th International Conference of B Users, pp. 79\u201393 (2006)","DOI":"10.1007\/11955757_9"},{"issue":"1","key":"516_CR26","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/s10472-010-9208-8","volume":"59","author":"M Leuschel","year":"2010","unstructured":"Leuschel, M., Massart, T.: Efficient approximate verification of B and Z models via symmetry markers. Ann. Math. Artif. Intell. 59(1), 81\u2013106 (2010)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1\u20132","key":"516_CR27","doi-asserted-by":"publisher","first-page":"53","DOI":"10.3233\/JCS-1998-61-204","volume":"6","author":"G Lowe","year":"1998","unstructured":"Lowe, G.: Casper: a compiler for the analysis of security protocols. J. Comput. Secur. 6(1\u20132), 53\u201384 (1998)","journal-title":"J. Comput. Secur."},{"key":"516_CR28","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Analysing lock-free linearizable datatypes using CSP. In: Concurrency, Security and Puzzles: Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday, volume 10160 of Lecture Notes in Computer Science, pp. 162\u2013184. Springer, New York (2017)","DOI":"10.1007\/978-3-319-51046-0_9"},{"key":"516_CR29","volume-title":"Distributed Algorithms","author":"N Lynch","year":"1996","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufmann, Burlington (1996)"},{"key":"516_CR30","doi-asserted-by":"crossref","unstructured":"Michael, M., Scott, M.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing, pp. 267\u2013275 (1996)","DOI":"10.1145\/248052.248106"},{"key":"516_CR31","doi-asserted-by":"publisher","unstructured":"Miller, A., Donaldson, A., Calder, M.: Symmetry in temporal logic model checking. ACM Comput. Surv. 38(3) (2006). \n                    https:\/\/doi.org\/10.1145\/1132960.1132962","DOI":"10.1145\/1132960.1132962"},{"key":"516_CR32","doi-asserted-by":"crossref","unstructured":"Moffat, N., Goldsmith, M., Roscoe, B.: A representative function approach to symmetry exploitation for CSP refinement checking. In: International Conference on Formal Engineering Methods. Lecture Notes in Computer Science, vol. 5256 (2008)","DOI":"10.1007\/978-3-540-88194-0_17"},{"issue":"1","key":"516_CR33","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/S0167-6423(00)00023-X","volume":"40","author":"A Mota","year":"2001","unstructured":"Mota, A., Sampaio, A.: Model-checking CSP-Z: strategy, tool support and industrial application. Sci. Comput. Program. 40(1), 59\u201396 (2001)","journal-title":"Sci. Comput. Program."},{"key":"516_CR34","unstructured":"Roscoe, A.W.: Model checking CSP. In: A Classical Mind: Essays in Honour of CAR Hoare. Prentice Hall, Hemel Hempstead (1994)"},{"key":"516_CR35","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0","volume-title":"Understanding Concurrent Systems","author":"AW Roscoe","year":"2010","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Springer, New York (2010)"},{"key":"516_CR36","unstructured":"Roscoe, A.W., Hopkins, D.: SVA: A tool for analysing shared-variable programs. In: Proceedings of Automatic Verification of Critical Systems (AVoCS), pp. 177\u2013183 (2007)"},{"key":"516_CR37","doi-asserted-by":"crossref","unstructured":"Schmidt, K.: Integrating low level symmetries into reachability analysis. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000). Lecture Notes in Computer Science, vol. 1785, pp. 315\u2013330 (2000)","DOI":"10.1007\/3-540-46419-0_22"},{"issue":"2","key":"516_CR38","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/350887.350891","volume":"9","author":"AP Sistla","year":"2000","unstructured":"Sistla, A.P., Gyuris, V., Emerson, E.A.: SMC: a symmetry-based model checker for verification of safety and liveness properties. ACM Trans. Softw. Eng. Methodol. 9(2), 133\u2013166 (2000)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"516_CR39","unstructured":"University of Oxford. FDR Documentation. \n                    http:\/\/www.cs.ox.ac.uk\/projects\/fdr\/manual\/index.html\n                    \n                   (2015). Accessed 19 Feb 2019"},{"key":"516_CR40","doi-asserted-by":"crossref","unstructured":"Valmari, A.: Stuborn sets for reduced state space generation. In: Advances in Petri Nets 1990. Lecture Notes in Computer Science, vol. 483, pp. 491\u2013515. Springer, New York (1991)","DOI":"10.1007\/3-540-53863-1_36"},{"issue":"2","key":"516_CR41","doi-asserted-by":"publisher","first-page":"799","DOI":"10.3390\/sym2020799","volume":"2","author":"T Wahl","year":"2010","unstructured":"Wahl, T., Donaldson, A.F.: Replication and abstraction: symmetry in automated formal verification. Symmetry 2(2), 799\u2013847 (2010)","journal-title":"Symmetry"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00516-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-019-00516-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00516-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,30]],"date-time":"2020-03-30T23:17:50Z","timestamp":1585610270000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-019-00516-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,4,1]]},"references-count":41,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2019,10]]}},"alternative-id":["516"],"URL":"https:\/\/doi.org\/10.1007\/s10009-019-00516-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,4,1]]},"assertion":[{"value":"1 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}