{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:47:04Z","timestamp":1725540424443},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642050886"},{"type":"electronic","value":"9783642050893"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-05089-3_45","type":"book-chapter","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T22:31:40Z","timestamp":1257287500000},"page":"708-723","source":"Crossref","is-referenced-by-count":16,"title":["Automated Property Verification for Large Scale B Models"],"prefix":"10.1007","author":[{"given":"Michael","family":"Leuschel","sequence":"first","affiliation":[]},{"given":"J\u00e9r\u00f4me","family":"Falampin","sequence":"additional","affiliation":[]},{"given":"Fabian","family":"Fritz","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Plagge","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"45_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"588","DOI":"10.1007\/11901433_32","volume-title":"Formal Methods and Software Engineering","author":"J.-R. Abrial","year":"2006","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 588\u2013605. Springer, Heidelberg (2006)"},{"unstructured":"Ambert, F., Bouquet, F., Chemin, S., Guenaud, S., Legeard, B., Peureux, F., Utting, M., Vacelet, N.: BZ-testing-tools: A tool-set for test generation from Z and B using constraint logic programming. In: Proceedings of FATES 2002, August 2002, pp. 105???120 (2002);","key":"#cr-split#-45_CR2.1"},{"unstructured":"Technical Report, INRIA","key":"#cr-split#-45_CR2.2"},{"key":"45_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/11415787_20","volume-title":"ZB 2005: Formal Specification and Development in Z and B","author":"F. Badeau","year":"2005","unstructured":"Badeau, F., Amelot, A.: Using B as a high level programming language in an industrial project: Roissy VAL. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol.\u00a03455, pp. 334\u2013354. Springer, Heidelberg (2005)"},{"key":"45_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-48119-2_22","volume-title":"FM\u201999 - Formal Methods","author":"P. Behm","year":"1999","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: M\u00e9t\u00e9or: A successful application of B in a large project. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 369\u2013387. Springer, Heidelberg (1999)"},{"key":"45_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/3-540-46002-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Bouquet","year":"2002","unstructured":"Bouquet, F., Legeard, B., Peureux, F.: CLPS-B - a constraint solver for B. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 188\u2013204. Springer, Heidelberg (2002)"},{"key":"45_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"678","DOI":"10.1007\/11901433_37","volume-title":"Formal Methods and Software Engineering","author":"J. Derrick","year":"2006","unstructured":"Derrick, J., North, S., Simons, T.: Issues in implementing a model checker for Z. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 678\u2013696. Springer, Heidelberg (2006)"},{"issue":"1","key":"45_CR7","doi-asserted-by":"publisher","first-page":"11","DOI":"10.3166\/tsi.22.11-32","volume":"22","author":"D. Doll\u00e9","year":"2003","unstructured":"Doll\u00e9, D., Essam\u00e9, D., Falampin, J.: B dans le tranport ferroviaire. L\u2019exp\u00e9rience de Siemens Transportation Systems. Technique et Science Informatiques\u00a022(1), 11\u201332 (2003)","journal-title":"Technique et Science Informatiques"},{"key":"45_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"45_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11955757_21","volume-title":"B 2007: Formal Specification and Development in B","author":"D. Essam\u00e9","year":"2006","unstructured":"Essam\u00e9, D., Doll\u00e9, D.: B in large-scale projects: The Canarsie line CBTC experience. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol.\u00a04355, pp. 252\u2013254. Springer, Heidelberg (2006)"},{"key":"45_CR10","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: A lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology\u00a011, 256\u2013290 (2002)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"45_CR11","volume-title":"Software Abstractions: Logic, Language and Analysis","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language and Analysis. MIT Press, Cambridge (2006)"},{"key":"45_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/3-540-45614-7_2","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"B. Legeard","year":"2002","unstructured":"Legeard, B., Peureux, F., Utting, M.: Automated boundary testing from Z and B. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 21\u201340. Springer, Heidelberg (2002)"},{"key":"45_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M. Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: A model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 855\u2013874. Springer, Heidelberg (2003)"},{"key":"45_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/11955757_9","volume-title":"B 2007: Formal Specification and Development in B","author":"M. Leuschel","year":"2006","unstructured":"Leuschel, M., Butler, M., Spermann, C., Turner, E.: Symmetry reduction for B by permutation flooding. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol.\u00a04355, pp. 79\u201393. Springer, Heidelberg (2006)"},{"issue":"2","key":"45_CR15","doi-asserted-by":"publisher","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\u00a010(2), 185\u2013203 (2008)","journal-title":"STTT"},{"unstructured":"Leuschel, M., Plagge, D.: Seven at a stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. In: Ameur, Y.A., Boniol, F., Wiels, V. (eds.) Proceedings Isola 2007. Revue des Nouvelles Technologies de l\u2019Information, vol.\u00a0RNTI-SM-1, pp. 73\u201384. C\u00e9padu\u00e8s-\u00c9ditions (2007)","key":"45_CR16"},{"unstructured":"Leuschel, M., Samia, M., Bendisposto, J., Luo, L.: Easy Graphical Animation and Formula Viewing for Teaching B. In: The B Method: from Research to Teaching, pp. 17\u201332 (2008)","key":"45_CR17"},{"key":"45_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/11955757_28","volume-title":"B 2007: Formal Specification and Development in B","author":"T. Servat","year":"2006","unstructured":"Servat, T.: Brama: A new graphic animation tool for B models. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol.\u00a04355, pp. 274\u2013276. Springer, Heidelberg (2006)"},{"unstructured":"Steria, F.: Aix-en-Provence. Atelier B, User and Reference Manuals (1996), \n                    \n                      http:\/\/www.atelierb.societe.com","key":"45_CR19"},{"unstructured":"Tatibouet, B.: The jbtools package (2001), \n                    \n                      http:\/\/lifc.univ-fcomte.fr\/PEOPLE\/tatibouet\/JBTOOLS\/BParser_en.html","key":"45_CR20"},{"key":"45_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 632\u2013647. Springer, Heidelberg (2007)"},{"key":"45_CR22","first-page":"25","volume-title":"Proceedings Symposium TASE 2007","author":"E. Turner","year":"2007","unstructured":"Turner, E., Leuschel, M., Spermann, C., Butler, M.: Symmetry reduced model checking for B. In: Proceedings Symposium TASE 2007, Shanghai, China, June 2007, pp. 25\u201334. IEEE, Los Alamitos (2007)"},{"key":"45_CR23","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1145\/996841.996859","volume-title":"PLDI 2004: Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation","author":"J. Whaley","year":"2004","unstructured":"Whaley, J., Lam, M.S.: Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In: PLDI 2004: Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, pp. 131\u2013144. ACM Press, New York (2004)"}],"container-title":["Lecture Notes in Computer Science","FM 2009: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-05089-3_45.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T11:19:05Z","timestamp":1619781545000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-05089-3_45"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642050886","9783642050893"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-05089-3_45","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}