{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T04:59:30Z","timestamp":1773723570564,"version":"3.50.1"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,5,1]],"date-time":"2010-05-01T00:00:00Z","timestamp":1272672000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2010,5]]},"DOI":"10.1007\/s10472-010-9208-8","type":"journal-article","created":{"date-parts":[[2010,8,13]],"date-time":"2010-08-13T02:42:19Z","timestamp":1281667339000},"page":"81-106","source":"Crossref","is-referenced-by-count":10,"title":["Efficient approximate verification of B and Z models via symmetry markers"],"prefix":"10.1007","volume":"59","author":[{"given":"Michael","family":"Leuschel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thierry","family":"Massart","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,8,14]]},"reference":[{"key":"9208_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"9208_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"9208_CR3","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S.: An open extensible tool environment for Event-B. In: ICFEM06, LNCS 4260, pp. 588\u2013605. Springer (2006)","DOI":"10.1007\/11901433_32"},{"key":"9208_CR4","unstructured":"B-Core (UK) Ltd, Oxon, UK. B-Toolkit, On-line manual. Available at http:\/\/www.b-core.com\/ONLINEDOC\/Contents.html (1999). Accessed 10 August 2010"},{"issue":"1\u20132","key":"9208_CR5","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/s10703-005-2246-x","volume":"27","author":"S Barner","year":"2005","unstructured":"Barner, S., Grumberg, O.: Combining symmetry reduction and under-approximation for symbolic model checking. Form. Methods Syst. Des. 27(1\u20132), 29\u201366 (2005)","journal-title":"Form. Methods Syst. Des."},{"key":"9208_CR6","unstructured":"Ben-Ari, M.: Principles of the Spin Model Checker. Springer (2008)"},{"issue":"1","key":"9208_CR7","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/s100090200074","volume":"4","author":"D Bosnacki","year":"2002","unstructured":"Bosnacki, D., Dams, D., Holenderski, L.: Symmetric spin. STTT 4(1), 92\u2013106 (2002)","journal-title":"STTT"},{"key":"9208_CR8","doi-asserted-by":"crossref","unstructured":"Bosnacki, D., Donaldson, A.F., Leuschel, M., Massart, T.: Efficient approximate verification of promela models via symmetry markers. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) Proceedings ATVA 2007, LNCS 4762, pp. 300\u2013315. Springer (2007)","DOI":"10.1007\/978-3-540-75596-8_22"},{"issue":"1\u20132","key":"9208_CR9","doi-asserted-by":"crossref","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. Des. 9(1\u20132), 77\u2013104 (1996)","journal-title":"Form. Methods Syst. Des."},{"key":"9208_CR10","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)"},{"key":"9208_CR11","unstructured":"ClearSy, Aix-en-Provence, France. B4Free: Tool and Manuals. Available at http:\/\/www.b4free.com (2006). Accessed 10 August 2010"},{"key":"9208_CR12","doi-asserted-by":"crossref","unstructured":"Derrick, J., North, S., Simons, A.: Z2sal: a translation-based model checker for z. Form. Asp. Comput. doi: 10.1007\/s00165-009-0126-7","DOI":"10.1007\/s00165-009-0126-7"},{"key":"9208_CR13","doi-asserted-by":"crossref","unstructured":"Derrick, J., North, S., Simons, A.J.H.: Z2SAL\u2014building a model checker for Z. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) Proceedings ABZ 2008, LNCS 5238, pp. 280\u2013293 (2008)","DOI":"10.1007\/978-3-540-87603-8_22"},{"key":"9208_CR14","doi-asserted-by":"crossref","unstructured":"Derrick, J., North, S., Simons, T.: Issues in implementing a model checker for Z. In: Liu, Z., He, J. (eds.) ICFEM, LNCS 4260, pp. 678\u2013696. Springer (2006)","DOI":"10.1007\/11901433_37"},{"key":"9208_CR15","doi-asserted-by":"crossref","unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: International Conference on Computer Design, pp. 522\u2013525 (1992)","DOI":"10.1109\/ICCD.1992.276232"},{"key":"9208_CR16","doi-asserted-by":"crossref","unstructured":"Donaldson, A.F., Miller, A.: Automatic symmetry detection for model checking using computational group theory. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) Proceedings FM 2005, LNCS 3582, pp. 481\u2013496. Springer (2005)","DOI":"10.1007\/11526841_32"},{"key":"9208_CR17","doi-asserted-by":"crossref","unstructured":"Donaldson, A.F., Miller, A.: Exact and approximate strategies for symmetry reduction in model checking. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) Proceedings FM\u20192006, LNCS 4085, pp. 541\u2013556. Springer (2006)","DOI":"10.1007\/11813040_36"},{"issue":"6","key":"9208_CR18","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/j.entcs.2005.04.010","volume":"128","author":"AF Donaldson","year":"2005","unstructured":"Donaldson, A.F., Miller, A., Calder, M.: Finding symmetry in models of concurrent systems by static channel diagram analysis. Electr. Notes Theor. Comput. Sci. 128(6), 161\u2013177 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1","key":"9208_CR19","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2005.09.007","volume":"139","author":"AF Donaldson","year":"2005","unstructured":"Donaldson, A.F., Miller, A., Calder, M.: Spin-to-grape: a tool for analysing symmetry in promela models. Electr. Notes Theor. Comput. Sci. 139(1), 3\u201323 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9208_CR20","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Sistla, A.P.: Utilizing symmetry when model checking under fairness assumptions: an automata-theoretic approach. In: Wolper, P. (ed.) Proceedings CAV\u201995, LNCS 939, pp. 309\u2013324. Springer (1995)","DOI":"10.1007\/3-540-60045-0_59"},{"issue":"1\/2","key":"9208_CR21","doi-asserted-by":"crossref","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. Des. 9(1\/2), 105\u2013131 (1996)","journal-title":"Form. Methods Syst. Des."},{"key":"9208_CR22","unstructured":"Flannery, S.: In Code: A Mathematical Adventure. Profile Books Ltd (2001)"},{"key":"9208_CR23","doi-asserted-by":"crossref","unstructured":"Hendriks, M., Behrmann, G., Larsen, K.G., Niebert, P., Vaandrager, F.W.: Adding symmetry reduction to Uppaal. In: Larsen, K.G., Niebert, P. (eds.) Proceedings FORMATS 2003, LNCS 2791, pp. 46\u201359. Springer (2003)","DOI":"10.1007\/978-3-540-40903-8_5"},{"issue":"2","key":"9208_CR24","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1002\/spe.4380180203","volume":"18","author":"GJ Holzmann","year":"1988","unstructured":"Holzmann, G.J.: An improved protocol reachability analysis technique. Softw. Pract. Exp. 18(2), 137\u2013161 (1988)","journal-title":"Softw. Pract. Exp."},{"issue":"5","key":"9208_CR25","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker spin. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9208_CR26","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley (2004)"},{"issue":"1\/2","key":"9208_CR27","first-page":"41","volume":"9","author":"CN Ip","year":"1996","unstructured":"Ip, C.N., Dill, D.L.: Better verification through symmetry. Form. Methods Syst. Des. 9(1\/2), 41\u201375 (1996)","journal-title":"Form. Methods Syst. Des."},{"issue":"2","key":"9208_CR28","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1145\/276393.276396","volume":"20","author":"D Jackson","year":"1998","unstructured":"Jackson, D., Jha, S., Damon, C.: Isomorph-free model enumeration: A new method for checking relational specifications. ACM Trans. Program. Lang. Syst. 20(2), 302\u2013343 (1998)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9208_CR29","unstructured":"Jha, S.: Semmetry and induction in model checking. PhD thesis, School of Computer Science, Carnegie Mellon University (1996)"},{"key":"9208_CR30","unstructured":"Kocay, W., Kreher, D.L.: Graphs, algorithms and optimization. Chapman & Hall\/CRC (2004)"},{"key":"9208_CR31","doi-asserted-by":"crossref","unstructured":"Kreher, D.L., Stinson, D.R.: Combinatorial Algorithms: Generation, Enumeration, Search. CRC Press (1999)","DOI":"10.1145\/309739.309744"},{"key":"9208_CR32","doi-asserted-by":"crossref","unstructured":"Leuschel, M.: The high road to formal validation. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) Proceedings ABZ 2008, LNCS 5238, pp. 4\u201323 (2008)","DOI":"10.1007\/978-3-540-87603-8_2"},{"key":"9208_CR33","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003: Formal Methods, LNCS 2805, pp. 855\u2013874. Springer (2003)","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"9208_CR34","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Butler, M.: Automatic refinement checking for B. In: Lau, K.-K., Banach, R. (eds.) Proceedings ICFEM\u201905, LNCS 3785, pp. 345\u2013359. Springer (2005)","DOI":"10.1007\/11576280_24"},{"key":"9208_CR35","first-page":"79","volume-title":"Proceedings B2007, LNCS 4355","author":"M Leuschel","year":"2007","unstructured":"Leuschel, M., Butler, M., Spermann, C., Turner, E.: Symmetry reduction for B by permutation flooding. In: Proceedings B2007, LNCS 4355, pp. 79\u201393. Springer, Besancon, France (2007)"},{"issue":"2","key":"9208_CR36","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2):185\u2013203 (2008)","journal-title":"STTT"},{"key":"9208_CR37","unstructured":"Leuschel, M., Massart, T.: Efficient approximate verification of B via symmetry markers. In: Proceedings International Symmetry Conference, pp. 71\u201385. Edinburgh, UK (2007)"},{"key":"9208_CR38","doi-asserted-by":"crossref","unstructured":"Manku, G.S., Hojati, R., Brayton, R.K.: Structural symmetry and model checking. In: Hu, A.J., Vardi, M.Y. (eds.) Proceedings CAV\u201998, LNCS 1427, pp. 159\u2013171. Springer (1998)","DOI":"10.1007\/BFb0028742"},{"key":"9208_CR39","doi-asserted-by":"crossref","unstructured":"Matos, P.J., Fischer, B., Silva, J.P.M.: A lazy unbounded model checker for event-b. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM of Lecture Notes in Computer Science, vol. 5885, pp. 485\u2013503. Springer (2009)","DOI":"10.1007\/978-3-642-10373-5_25"},{"key":"9208_CR40","unstructured":"McKay, B.: Nauty user\u2019s guide. Available via http:\/\/cs.anu.edu.au\/people\/bdm\/nauty\/ . Accessed 10 August 2010"},{"key":"9208_CR41","first-page":"45","volume":"30","author":"BD McKay","year":"1981","unstructured":"McKay, B.D.: Practical graph isomorphism. Congressus Numerantium. 30, 45\u201387 (1981)","journal-title":"Congressus Numerantium."},{"issue":"3","key":"9208_CR42","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1145\/1132960.1132962","volume":"38","author":"A Miller","year":"2006","unstructured":"Miller, A., Donaldson, A., Calder, M.: Symmetry in temporal logic model checking. ACM Comput. Surv. 38(3), 8 (2006)","journal-title":"ACM Comput. Surv."},{"issue":"3","key":"9208_CR43","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"GL Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115\u2013116 (1981)","journal-title":"Inf. Process. Lett."},{"key":"9208_CR44","doi-asserted-by":"crossref","unstructured":"Plagge, D., Leuschel, M.: Validating Z specificatons using the ProB animator and model checker. In: Davies, J., Gibbons, J. (eds.) Proceedings IFM 2007, LNCS 4591, pp. 480\u2013500. Springer (2007)","DOI":"10.1007\/978-3-540-73210-5_25"},{"key":"9208_CR45","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/s10009-009-0132-3","volume":"11","author":"D Plagge","year":"2010","unstructured":"Plagge, D., Leuschel, M.: Seven at a stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. STTT 11, 9\u201321 (2010)","journal-title":"STTT"},{"key":"9208_CR46","unstructured":"Schneider, S.: The B-method, An Introduction. Computer Science\u2014The Cornerstones of Computing Series. Palgrave, macmillan (2001)"},{"issue":"2","key":"9208_CR47","doi-asserted-by":"crossref","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":"9208_CR48","doi-asserted-by":"crossref","unstructured":"Spermann, C., Leuschel, M.: ProB gets nauty: effective symmetry reduction for B and Z models. In: Proceedings TASE 2008, pp. 15\u201322. IEEE, Nanjing, China (2008)","DOI":"10.1109\/TASE.2008.33"},{"key":"9208_CR49","unstructured":"France Steria, Aix-en-Provence: Atelier B, user and reference manuals. Available at http:\/\/www.atelierb.eu (1996). Accessed 10 August 2010"},{"key":"9208_CR50","doi-asserted-by":"crossref","unstructured":"Turner, E., Leuschel, M., Spermann, C., Butler, M.J.: Symmetry reduced model checking for B. In: Proceedings TASE 2007, pp. 25\u201334. IEEE Computer Society (2007)","DOI":"10.1109\/TASE.2007.50"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-010-9208-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-010-9208-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-010-9208-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T15:08:42Z","timestamp":1559401722000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-010-9208-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,5]]},"references-count":50,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,5]]}},"alternative-id":["9208"],"URL":"https:\/\/doi.org\/10.1007\/s10472-010-9208-8","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,5]]}}}