{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:36:34Z","timestamp":1771025794688,"version":"3.50.1"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319912707","type":"print"},{"value":"9783319912714","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-91271-4_6","type":"book-chapter","created":{"date-parts":[[2018,5,7]],"date-time":"2018-05-07T14:32:55Z","timestamp":1525703575000},"page":"71-86","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Translation from Alloy to B"],"prefix":"10.1007","author":[{"given":"Sebastian","family":"Krings","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joshua","family":"Schmidt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carola","family":"Brings","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Frappier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,8]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BFb0033845","volume-title":"Programming Languages: Implementations, Logics, and Programs","author":"M Carlsson","year":"1997","unstructured":"Carlsson, M., Ottosson, G., Carlson, B.: An open-ended finite domain constraint solver. In: Glaser, H., Hartel, P., Kuchen, H. (eds.) PLILP 1997. LNCS, vol. 1292, pp. 191\u2013206. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0033845"},{"key":"6_CR3","unstructured":"ClearSy: Atelier B, User and Reference Manuals. Aix-en-Provence, France (2009). http:\/\/www.atelierb.eu\/"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-662-43652-3_29","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"A Cunha","year":"2014","unstructured":"Cunha, A.: Bounded model checking of temporal formulas with Alloy. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 303\u2013308. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43652-3_29"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Frias, M.F., Galeotti, J.P., Pombo, C.L., Aguirre, N.: DynAlloy: upgrading alloy with actions. In: Proceedings of the ICSE, pp. 442\u2013451 (2005)","DOI":"10.1145\/1062455.1062535"},{"issue":"1","key":"6_CR6","doi-asserted-by":"publisher","first-page":"4:1","DOI":"10.1145\/1314493.1314497","volume":"17","author":"MF Frias","year":"2007","unstructured":"Frias, M.F., Pombo, C.L., Galeotti, J.P., Aguirre, N.: Efficient analysis of DynAlloy specifications. ACM Trans. Softw. Eng. Methodol. 17(1), 4:1\u20134:34 (2007)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"6_CR7","unstructured":"Ghazi, A.A.E., Taghdiri, M.: Analyzing alloy formulas using an SMT solver: a case study. CoRR, abs\/1505.00672 (2015)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-30729-4_3","volume-title":"Integrated Formal Methods","author":"D Hansen","year":"2012","unstructured":"Hansen, D., Leuschel, M.: Translating TLA+ to B for validation with ProB. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 24\u201338. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30729-4_3"},{"key":"6_CR9","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 Trans. Softw. Eng. Methodol. 11, 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"6_CR10","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":"6_CR11","unstructured":"Jaffar, J., Michaylov, S.: Methodology and implementation of a CLP system. In: Proceedings ICLP, pp. 196\u2013218. MIT Press (1987)"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Krings, S., Leuschel, M.: Constraint logic programming over infinite domains with an application to proof. In: Proceedings of WLP. Electronic Proceedings in Theoretical Computer Science, EPTCS, vol. 234 (2016)","DOI":"10.4204\/EPTCS.234.6"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-319-33693-0_23","volume-title":"Integrated Formal Methods","author":"S Krings","year":"2016","unstructured":"Krings, S., Leuschel, M.: SMT solvers for validation of B and Event-B models. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 361\u2013375. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_23"},{"key":"6_CR14","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.scico.2017.08.013","volume":"158","author":"S Krings","year":"2017","unstructured":"Krings, S., Leuschel, M.: Proof assisted bounded and unbounded symbolic model checking of software and system models. Sci. Comput. Program. 158, 41\u201363 (2017)","journal-title":"Sci. Comput. Program."},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-319-73305-0_5","volume-title":"Practical Aspects of Declarative Languages","author":"S Krings","year":"2018","unstructured":"Krings, S., Leuschel, M., K\u00f6rner, P., Hallerstede, S., Hasanagi\u0107, M.: Three is a crowd: SAT, SMT and CLP on a chessboard. In: Calimeri, F., Hamlen, K., Leone, N. (eds.) PADL 2018. LNCS, vol. 10702, pp. 63\u201379. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-73305-0_5"},{"key":"6_CR16","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1002\/9781119002727.ch14","volume-title":"Formal Methods Applied to Complex Systems: Implementation of the B Method","author":"M Leuschel","year":"2014","unstructured":"Leuschel, M., Bendisposto, J., Dobrikov, I., Krings, S., Plagge, D.: From animation to data validation: the ProB constraint solver 10 years on. In: Boulanger, J.-L. (ed.) Formal Methods Applied to Complex Systems: Implementation of the B Method, pp. 427\u2013446. Wiley ISTE, Hoboken (2014)"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. 2805, pp. 855\u2013874. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_46"},{"issue":"2","key":"6_CR18","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.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185\u2013203 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"6_CR19","unstructured":"Macedo, N., Cunha, A.: Alloy meets TLA+: an exploratory study. CoRR, abs\/1603.03599 (2016)"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-11811-1_28","volume-title":"Abstract State Machines, Alloy, B and Z","author":"P Malik","year":"2010","unstructured":"Malik, P., Groves, L., Lenihan, C.: Translating Z to Alloy. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 377\u2013390. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11811-1_28"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-87603-8_34","volume-title":"Abstract State Machines, B and Z","author":"PJ Matos","year":"2008","unstructured":"Matos, P.J., Marques-Silva, J.: Model checking Event-B by encoding into Alloy. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, p. 346. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-87603-8_34"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-63046-5_10","volume-title":"Automated Deduction \u2013 CADE 26","author":"B Meng","year":"2017","unstructured":"Meng, B., Reynolds, A., Tinelli, C., Barrett, C.: Relational constraint solving in SMT. In: de Moura, L. (ed.) CADE 2017. LNCS, vol. 10395, pp. 148\u2013165. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_10"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/3-540-45648-1_8","volume-title":"ZB 2002:Formal Specification and Development in Z and B","author":"L Mikhailov","year":"2002","unstructured":"Mikhailov, L., Butler, M.: An approach to combining B and Alloy. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 140\u2013161. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45648-1_8"},{"key":"6_CR24","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/j.scico.2014.05.009","volume":"94","author":"A Milicevic","year":"2014","unstructured":"Milicevic, A., Jackson, D.: Preventing arithmetic overflows in Alloy. Sci. Comput. Program. 94, 203\u2013216 (2014)","journal-title":"Sci. Comput. Program."},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. In: Formal Methods in System Design, January 2017","DOI":"10.1007\/s10703-016-0267-2"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-642-11811-1_10","volume-title":"Abstract State Machines, Alloy, B and Z","author":"JP Near","year":"2010","unstructured":"Near, J.P., Jackson, D.: An imperative extension to Alloy. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 118\u2013131. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11811-1_10"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-540-73210-5_25","volume-title":"Integrated Formal Methods","author":"D Plagge","year":"2007","unstructured":"Plagge, D., Leuschel, M.: Validating Z specifications using the ProB animator and model checker. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 480\u2013500. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73210-5_25"},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-32759-9_31","volume-title":"FM 2012: Formal Methods","author":"D Plagge","year":"2012","unstructured":"Plagge, D., Leuschel, M.: Validating B,Z and TLA+ using ProB\u00a0and Kodkod. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 372\u2013386. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_31"},{"key":"6_CR29","unstructured":"S\u00fclflow, A., K\u00fchne, U., Wille, R., Gro\u00dfe, D., Drechsler, R.: Evaluation of SAT-like proof techniques for formal verification of word-level circuits. In: Proceedings IEEE WRTLT, Beijing, China. IEEE Computer Society Press, October 2007"},{"key":"6_CR30","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. 4424, pp. 632\u2013647. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_49"},{"issue":"4","key":"6_CR31","doi-asserted-by":"publisher","first-page":"915","DOI":"10.1017\/S0960129512000291","volume":"23","author":"E Torlak","year":"2013","unstructured":"Torlak, E., Taghdiri, M., Dennis, G., Near, J.P.: Applications and extensions of Alloy: past, present and future. Math. Struct. Comput. Sci. 23(4), 915\u2013933 (2013)","journal-title":"Math. Struct. Comput. Sci."},{"key":"6_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-642-28756-5_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Ulbrich","year":"2012","unstructured":"Ulbrich, M., Geilmann, U., El Ghazi, A.A., Taghdiri, M.: A proof assistant for Alloy specifications. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 422\u2013436. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_29"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, TLA, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-91271-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T13:29:29Z","timestamp":1693661369000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-91271-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319912707","9783319912714"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-91271-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}