{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,17]],"date-time":"2026-01-17T08:40:47Z","timestamp":1768639247964,"version":"3.49.0"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319406473","type":"print"},{"value":"9783319406480","type":"electronic"}],"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-40648-0_13","type":"book-chapter","created":{"date-parts":[[2016,6,3]],"date-time":"2016-06-03T09:42:13Z","timestamp":1464946933000},"page":"166-171","source":"Crossref","is-referenced-by-count":20,"title":["EventB2Java: A Code Generator for Event-B"],"prefix":"10.1007","author":[{"given":"N\u00e9stor","family":"Cata\u00f1o","sequence":"first","affiliation":[]},{"given":"V\u00edctor","family":"Rivera","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,4]]},"reference":[{"key":"13_CR1","unstructured":"Abrial, J.-R.: Sequential Program Development: Teaching Resources (2009). http:\/\/deploy-eprints.ecs.soton.ac.uk\/122\/1\/sld.ch15%2Cseq.pdf . Accessed 2015"},{"key":"13_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Design","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Design. Cambridge University Press, New York (2010)"},{"issue":"6","key":"13_CR3","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010)","journal-title":"Softw. Tools Technol. Transf."},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/978-3-642-04912-5_2","volume-title":"Teaching Formal Methods","author":"N Catano","year":"2009","unstructured":"Catano, N., Rueda, C.: Teaching formal methods for the unconquered territory. In: Gibbons, J., Oliveira, J.N. (eds.) TFM 2009. LNCS, vol. 5846, pp. 2\u201319. Springer, Heidelberg (2009)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1007\/978-3-642-11811-1_20","volume-title":"Abstract State Machines, Alloy, B and Z","author":"N Catano","year":"2010","unstructured":"Catano, N., Rueda, C.: Matelas: a predicate calculus common formal definition for social networking. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 259\u2013272. Springer, Heidelberg (2010)"},{"key":"13_CR6","unstructured":"Edmunds, A., Butler, M.: Tool support for Event-B code generation. In: Workshop on Tool Building in Formal Methods, Qu\u00e9bec, Canada. John Wiley and Sons (2010)"},{"key":"13_CR7","unstructured":"Edmunds, A., Rezazedeh, A.: Development of a Heating Controller System (2011). http:\/\/wiki.event-b.org\/index.php\/Development_of_a_Heating_Controller_System . Accessed Mar 2015"},{"issue":"3","key":"13_CR8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"G Leavens","year":"2006","unstructured":"Leavens, G., Baker, A., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. ACM Spec. Interest Group Softw. Eng. 31(3), 1\u201338 (2006)","journal-title":"ACM Spec. Interest Group Softw. Eng."},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"M\u00e9ry, D., Singh, N.: Automatic code generation from Event-B models. In: Symposium on Information and Communication Technology, Hanoi, Vietnam. ACM (2011)","DOI":"10.1145\/2069216.2069252"},{"key":"13_CR10","volume-title":"Object-Oriented Software Construction","author":"B Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall Inc, Upper Saddle River (1997)","edition":"2"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Ostroumov, S., Tsiopoulos, L.: VHDL code generation from formal Event-B models. In: Euromicro Conference on Digital System Design, pp. 127\u2013134 (2011)","DOI":"10.1109\/DSD.2011.20"},{"key":"13_CR12","unstructured":"V\u00edctor, R., Cata\u00f1o, N.: The Social-Event Planner (2012). http:\/\/poporo.uma.pt\/favas\/Social-Event_Planner.html . Accessed 2015"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Rivera, V., Cata\u00f1o, N.: Translating Event-B to JML-specified Java programs. In: 29th ACM SAC, Gyeongju, South Korea, 24\u201328 March 2014","DOI":"10.1145\/2554850.2554897"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Rivera, V., Cata\u00f1o, N., Wahls, T., Rueda, C.: Code generation for Event-B. Int. J. Softw. Tools Technol. Transf. (STTT), pp. 1\u201322 (2015)","DOI":"10.1007\/s10009-015-0381-2"},{"key":"13_CR15","unstructured":"State-Machines and Code Generation (2012). http:\/\/wiki.event-b.org\/index.php\/State-Machines_and_Code_Generation . Accessed Aug 2013"},{"key":"13_CR16","unstructured":"Wright, S.: Automatic generation of C from Event-B. In: Workshop on Integration of Model-based Formal Methods and Tools, Nantes, France. Springer-Verlag (2009)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40648-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T11:41:24Z","timestamp":1498304484000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40648-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319406473","9783319406480"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40648-0_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}