{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T13:48:56Z","timestamp":1762955336047,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,3,24]],"date-time":"2014-03-24T00:00:00Z","timestamp":1395619200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,3,24]]},"DOI":"10.1145\/2554850.2554897","type":"proceedings-article","created":{"date-parts":[[2014,7,22]],"date-time":"2014-07-22T15:08:30Z","timestamp":1406041710000},"page":"1264-1271","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Translating event-B to JML-specified Java programs"],"prefix":"10.1145","author":[{"given":"V\u00edctor","family":"Rivera","sequence":"first","affiliation":[{"name":"The University of Madeira"}]},{"given":"N\u00e9stor","family":"Cata\u00f1o","sequence":"additional","affiliation":[{"name":"University EAFIT"}]}],"member":"320","published-online":{"date-parts":[[2014,3,24]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"J.-R. Abrial. Sequential program development: Teaching resources. http:\/\/deploy-eprints.ecs.soton.ac.uk\/122\/1\/sld.ch15\\%2Cseq.pdf 2009.  J.-R. Abrial. Sequential program development: Teaching resources. http:\/\/deploy-eprints.ecs.soton.ac.uk\/122\/1\/sld.ch15\\%2Cseq.pdf 2009."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855020"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0145-y"},{"key":"e_1_3_2_1_4_1","unstructured":"J.-R. Abrial and S. Hallerstede. Refinement decomposition and instantiation of discrete models: Application to Event-B. Fundamentae Informatica 77(1 2): 1--24 2007.   J.-R. Abrial and S. Hallerstede. Refinement decomposition and instantiation of discrete models: Application to Event-B. Fundamentae Informatica 77(1 2): 1--24 2007."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.05.011"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00255-7_2"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"N. Cata\u00f1o C. Rueda and T. Wahls. A Machine-Checked Proof for a Translation of Event-B Machines to JML. ArXiv e-prints September 2013.  N. Cata\u00f1o C. Rueda and T. Wahls. A Machine-Checked Proof for a Translation of Event-B Machines to JML. ArXiv e-prints September 2013.","DOI":"10.1002\/9781119002727.ch9"},{"key":"e_1_3_2_1_8_1","unstructured":"N.\n       \n      Cata\u00f1o\n     and \n      \n      \n      M.\n       \n      Huisman\n      \n  \n  . \n  Chase: A static checker for JML's assignable clause. In L. Zuck P. Attie A. Cortesi and S. Mukhopadhyay editors VMCAI volume \n  2575\n   of \n  LNCS pages \n  26\n  --\n  40 New York NY USA January 9--11 \n  2003\n  . \n  Springer-Verlag\n  .   N. Cata\u00f1o and M. Huisman. Chase: A static checker for JML's assignable clause. In L. Zuck P. Attie A. Cortesi and S. Mukhopadhyay editors VMCAI volume 2575 of LNCS pages 26--40 New York NY USA January 9--11 2003. Springer-Verlag."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04912-5_2"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11811-1_20"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1529282.1529373"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2245276.2231978"},{"key":"e_1_3_2_1_13_1","first-page":"472","volume-title":"NFM","author":"Cok D.","year":"2011"},{"volume-title":"University of Southampton","year":"2010","author":"Damchoom K.","key":"e_1_3_2_1_14_1"},{"volume-title":"WS-TBFM2010","year":"2010","author":"Edmunds A.","key":"e_1_3_2_1_15_1"},{"volume-title":"PLACES","year":"2011","author":"Edmunds A.","key":"e_1_3_2_1_16_1"},{"key":"e_1_3_2_1_17_1","unstructured":"A. Edmunds and A. Rezazedah. Development of a Heating Controller System 2011. Available at http:\/\/wiki.eventb.org\/index.php\/Development_of_a_Heating_Controller_System.  A. Edmunds and A. Rezazedah. Development of a Heating Controller System 2011. Available at http:\/\/wiki.eventb.org\/index.php\/Development_of_a_Heating_Controller_System."},{"key":"e_1_3_2_1_18_1","unstructured":"Google Inc. The Android Platform. http:\/\/developer.android.com\/design\/index.html 2012.  Google Inc. The Android Platform. http:\/\/developer.android.com\/design\/index.html 2012."},{"key":"e_1_3_2_1_19_1","series-title":"LNCS","volume-title":"Proceedings of FMICS","author":"Krause B.","year":"2006"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/361082.361093"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"volume-title":"Wrox","year":"2012","author":"Mejer R.","key":"e_1_3_2_1_22_1"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2069216.2069252"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSD.2011.20"},{"key":"e_1_3_2_1_25_1","unstructured":"V. Rivera and N. Cata\u00f1o. The Social-Event Planner 2012. Available at http:\/\/poporo.uma.pt\/Projects\/favas\/Social-Event_Planner.html.  V. Rivera and N. Cata\u00f1o. The Social-Event Planner 2012. Available at http:\/\/poporo.uma.pt\/Projects\/favas\/Social-Event_Planner.html."},{"key":"e_1_3_2_1_26_1","unstructured":"State-Machines and Code Generation 2013. Available at http:\/\/wiki.event-b.org\/index.php\/State-Machines_and_Code_Generation.  State-Machines and Code Generation 2013. Available at http:\/\/wiki.event-b.org\/index.php\/State-Machines_and_Code_Generation."},{"volume-title":"Workshop on IM_FMT","year":"2009","author":"Wright S.","key":"e_1_3_2_1_27_1"}],"event":{"name":"SAC 2014: Symposium on Applied Computing","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"],"location":"Gyeongju Republic of Korea","acronym":"SAC 2014"},"container-title":["Proceedings of the 29th Annual ACM Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2554850.2554897","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2554850.2554897","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:18:16Z","timestamp":1750234696000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2554850.2554897"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3,24]]},"references-count":27,"alternative-id":["10.1145\/2554850.2554897","10.1145\/2554850"],"URL":"https:\/\/doi.org\/10.1145\/2554850.2554897","relation":{},"subject":[],"published":{"date-parts":[[2014,3,24]]},"assertion":[{"value":"2014-03-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}