{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T05:41:58Z","timestamp":1757310118863,"version":"3.41.0"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319335995"},{"type":"electronic","value":"9783319336008"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-33600-8_11","type":"book-chapter","created":{"date-parts":[[2016,5,10]],"date-time":"2016-05-10T08:15:15Z","timestamp":1462868115000},"page":"183-197","source":"Crossref","is-referenced-by-count":6,"title":["Generating Event-B Specifications from Algorithm Descriptions"],"prefix":"10.1007","author":[{"given":"Joy","family":"Clark","sequence":"first","affiliation":[]},{"given":"Jens","family":"Bendisposto","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Hallerstede","sequence":"additional","affiliation":[]},{"given":"Dominik","family":"Hansen","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,5,11]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)","edition":"1"},{"key":"11_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book. Cambridge University Press, New York (1996)"},{"key":"11_CR3","volume-title":"The B-Method: An Introduction","author":"S Schneider","year":"2001","unstructured":"Schneider, S.: The B-Method: An Introduction. Palgrave Macmillan, Basingstoke (2001)"},{"key":"11_CR4","unstructured":"Lecomte, T.: Ten years disseminating the B method. In: Attiogbe, C., Mery, D. (eds.) Proceedings of TFM-B 2010, pp. 65\u201372. APCB, June 2010"},{"issue":"1","key":"11_CR5","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s00165-011-0205-4","volume":"24","author":"S Hallerstede","year":"2012","unstructured":"Hallerstede, S., Leuschel, M.: Experiments in program verification using Event-B. Formal Aspects Comput. 24(1), 97\u2013125 (2012)","journal-title":"Formal Aspects Comput."},{"issue":"1","key":"11_CR6","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/1125808.1125811","volume":"15","author":"CF Snook","year":"2006","unstructured":"Snook, C.F., Butler, M.J.: UML-B: formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92\u2013122 (2006)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"2\u20133","key":"11_CR7","first-page":"197","volume":"3","author":"D M\u00e9ry","year":"2009","unstructured":"M\u00e9ry, D.: Refinement-based guidelines for algorithmic systems. Int. J. Softw. Inf. 3(2\u20133), 197\u2013239 (2009)","journal-title":"Int. J. Softw. Inf."},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/978-3-642-24124-6_2","volume-title":"Software Engineering for Resilient Systems","author":"A Iliasov","year":"2011","unstructured":"Iliasov, A.: Use case scenarios as verification conditions: event-B\/Flow approach. In: Troubitsyna, E.A. (ed.) SERENE 2011. LNCS, vol. 6968, pp. 9\u201323. Springer, Heidelberg (2011)"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-642-30885-7_33","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"A Edmunds","year":"2012","unstructured":"Edmunds, A., Butler, M., Maamria, I., Silva, R., Lovell, C.: Event-B code generation: type extension with theories. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 365\u2013368. Springer, Heidelberg (2012)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/978-3-662-43652-3_25","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"A Edmunds","year":"2014","unstructured":"Edmunds, A.: Templates for Event-B code generation. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 284\u2013289. Springer, Heidelberg (2014)"},{"issue":"1","key":"11_CR11","first-page":"65","volume":"8","author":"D Petit","year":"2004","unstructured":"Petit, D., Poirriez, V., Mariano, G.: The B method and the component-based approach. Trans. SDPS 8(1), 65\u201376 (2004)","journal-title":"Trans. SDPS"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-540-45236-2_7","volume-title":"FME 2003: Formal Methods","author":"D Bert","year":"2003","unstructured":"Bert, D., Boulm\u00e9, S., Potet, M.-L., Requet, A., Voisin, L.: Adaptable translator of B specifications to embedded C programs. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 94\u2013113. Springer, Heidelberg (2003)"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-540-87603-8_33","volume-title":"Abstract State Machines, B and Z","author":"A Requet","year":"2008","unstructured":"Requet, A.: BART: a tool for automatic refinement. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, p. 345. Springer, Heidelberg (2008)"},{"key":"11_CR14","volume-title":"Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods","author":"Y Yu","year":"1999","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54\u201366. Springer, Heidelberg (1999)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-14203-1_12","volume-title":"Automated Reasoning","author":"K Chaudhuri","year":"2010","unstructured":"Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: Verifying safety properties with the TLA + proof system. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 142\u2013148. Springer, Heidelberg (2010)"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Rustan, K., Leino, M.: Developing verified programs with dafny. In: Proceedings ICSE 2013, pp. 1488\u20131490 (2013)","DOI":"10.1109\/ICSE.2013.6606754"},{"key":"11_CR18","unstructured":"Koenig, J., Rustan, K., Leino, M.: Getting started with dafny: a guide. In: Nipkow, T., Grumberg, O., Hauptmann, B. (eds.) Software Safety and Security - Tools for Analysis and Verification. NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 33, pp. 152\u2013181. IOS Press (2012)"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-642-12002-2_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M., R\u00fcmmer, P.: A polymorphic intermediate verification language: design and logical encoding. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 312\u2013327. Springer, Heidelberg (2010)"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-30885-7_14","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"D D\u00e9harbe","year":"2012","unstructured":"D\u00e9harbe, D., Fontaine, P., Guyot, Y., Voisin, L.: SMT solvers for rodin. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 194\u2013207. Springer, Heidelberg (2012)"},{"issue":"7","key":"11_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/390013.808479","volume":"5","author":"FE Allen","year":"1970","unstructured":"Allen, F.E.: Control flow analysis. SIGPLAN Not. 5(7), 1\u201319 (1970)","journal-title":"SIGPLAN Not."},{"issue":"1","key":"11_CR22","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s00165-009-0138-3","volume":"23","author":"S Hallerstede","year":"2011","unstructured":"Hallerstede, S.: On the purpose of Event-B proof obligations. Formal Asp. Comput 23(1), 133\u2013150 (2011)","journal-title":"Formal Asp. Comput"}],"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-33600-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T02:34:48Z","timestamp":1748918088000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33600-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319335995","9783319336008"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33600-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}