{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:50:36Z","timestamp":1750308636078,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2012,3,26]],"date-time":"2012-03-26T00:00:00Z","timestamp":1332720000000},"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":[[2012,3,26]]},"DOI":"10.1145\/2245276.2231978","type":"proceedings-article","created":{"date-parts":[[2012,6,11]],"date-time":"2012-06-11T13:03:31Z","timestamp":1339419811000},"page":"1271-1277","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Translating B machines to JML specifications"],"prefix":"10.1145","author":[{"given":"N\u00e9stor","family":"Cata\u00f1o","sequence":"first","affiliation":[{"name":"The University of Madeira"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tim","family":"Wahls","sequence":"additional","affiliation":[{"name":"Dickinson College"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Camilo","family":"Rueda","sequence":"additional","affiliation":[{"name":"Pontificia Universidad Javeriana"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"V\u00edctor","family":"Rivera","sequence":"additional","affiliation":[{"name":"The University of Madeira"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Danni","family":"Yu","sequence":"additional","affiliation":[{"name":"Dickinson College"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,3,26]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Electronic Notes in Theoretical Computer Science","author":"Abdennadher S.","year":"2002","unstructured":"S. Abdennadher , E. Kr\u00e4mer , M. Saft , and M. Schmauss . JACK: A Java constraint kit . In M. Hanus, editor, Electronic Notes in Theoretical Computer Science , volume 64 . Elsevier , 2002 . S. Abdennadher, E. Kr\u00e4mer, M. Saft, and M. Schmauss. JACK: A Java constraint kit. In M. Hanus, editor, Electronic Notes in Theoretical Computer Science, volume 64. Elsevier, 2002."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/236705"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855020"},{"key":"e_1_3_2_1_4_1","unstructured":"Atelier B. http:\/\/www.atelierb.eu\/index_en.html.  Atelier B. http:\/\/www.atelierb.eu\/index_en.html."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_3_2_1_6_1","volume-title":"Proceedings of ACSD","author":"Boulanger J.-L.","year":"2003","unstructured":"J.-L. Boulanger . ABTools : Another B tool . In Proceedings of ACSD , 2003 . J.-L. Boulanger. ABTools: Another B tool. In Proceedings of ACSD, 2003."},{"key":"e_1_3_2_1_7_1","first-page":"2855","volume-title":"Information and Communication Technologies","volume":"2","author":"Boulanger J.-L.","year":"2006","unstructured":"J.-L. Boulanger . B\/HDL : design of safety circuit . In Information and Communication Technologies , volume 2 , pages 2855 -- 2860 , 2006 . J.-L. Boulanger. B\/HDL: design of safety circuit. In Information and Communication Technologies, volume 2, pages 2855--2860, 2006."},{"key":"e_1_3_2_1_8_1","unstructured":"J.-L. Boulanger. The ABTools Suite. http:\/\/sourceforge.net\/projects\/abtools\/ 2011.  J.-L. Boulanger. The ABTools Suite. http:\/\/sourceforge.net\/projects\/abtools\/ 2011."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11415787_25"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11955757_31"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_3_2_1_12_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1007\/3-540-36384-X_6","volume-title":"Proceedings of VMCAI","author":"Cata\u00f1o N.","year":"2003","unstructured":"N. Cata\u00f1o and M. Huisman . Chase: A static checker for JML's assignable clause . In L. D. Zuck, P. C. Attie, A. Cortesi, and S. Mukhopadhyay, editors, Proceedings of VMCAI , volume 2575 of Lecture Notes in Computer Science , pages 26 -- 40 , New York, NY , USA, January 9--11 2003 . Springer-Verlag . N. Cata\u00f1o and M. Huisman. Chase: A static checker for JML's assignable clause. In L. D. Zuck, P. C. Attie, A. Cortesi, and S. Mukhopadhyay, editors, Proceedings of VMCAI, volume 2575 of Lecture Notes in Computer Science, pages 26--40, New York, NY, USA, January 9--11 2003. Springer-Verlag."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11811-1_20"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1529282.1529373"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_16"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1986308.1986347"},{"key":"e_1_3_2_1_17_1","volume-title":"Computer Science Laboratory","author":"Duterte B.","year":"2006","unstructured":"B. Duterte and L. de Moura . The YICES SMT solver. Technical report , Computer Science Laboratory , SRI International , 2006 . B. Duterte and L. de Moura. The YICES SMT solver. Technical report, Computer Science Laboratory, SRI International, 2006."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_11"},{"key":"e_1_3_2_1_19_1","first-page":"288","volume":"4790","author":"Dubois C.","year":"2007","unstructured":"\u00c9. Jaeger and C. Dubois . Why would you trust B? In Proceedings of LPAR , volume 4790 of LNCS, pages 288 -- 302 , 2007 . \u00c9. Jaeger and C. Dubois. Why would you trust B? In Proceedings of LPAR, volume 4790 of LNCS, pages 288--302, 2007.","journal-title":"In Proceedings of LPAR"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/ALPIT.2008.25"},{"key":"e_1_3_2_1_21_1","series-title":"Lecture Notes in Computer Science","first-page":"293","volume-title":"Proceedings of FMICS","author":"Krause B.","year":"2006","unstructured":"B. Krause and T. Wahls . jmle: A tool for executing JML specifications via constraint programming . In L. Brim, editor, Proceedings of FMICS , volume 4346 of Lecture Notes in Computer Science , pages 293 -- 296 . Springer-Verlag , August 2006 . B. Krause and T. Wahls. jmle: A tool for executing JML specifications via constraint programming. In L. Brim, editor, Proceedings of FMICS, volume 4346 of Lecture Notes in Computer Science, pages 293--296. Springer-Verlag, August 2006."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1884866.1884879"},{"key":"e_1_3_2_1_24_1","series-title":"Series in Computer Science","volume-title":"Object Oriented Software Construction","author":"Meyer B.","year":"1998","unstructured":"B. Meyer . Object Oriented Software Construction . Series in Computer Science . Prentice Hall International , 1998 . B. Meyer. Object Oriented Software Construction. Series in Computer Science. Prentice Hall International, 1998."},{"key":"e_1_3_2_1_25_1","volume-title":"Pragmatic Bookshelf","author":"Parr T.","year":"2007","unstructured":"T. Parr . The Definitive ANTLR Reference: Building Domain-Specific Languages . Pragmatic Bookshelf , 2007 . T. Parr. The Definitive ANTLR Reference: Building Domain-Specific Languages. Pragmatic Bookshelf, 2007."}],"event":{"name":"SAC 2012: ACM Symposium on Applied Computing","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"],"location":"Trento Italy","acronym":"SAC 2012"},"container-title":["Proceedings of the 27th Annual ACM Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2245276.2231978","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2245276.2231978","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:08:04Z","timestamp":1750273684000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2245276.2231978"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,26]]},"references-count":25,"alternative-id":["10.1145\/2245276.2231978","10.1145\/2245276"],"URL":"https:\/\/doi.org\/10.1145\/2245276.2231978","relation":{},"subject":[],"published":{"date-parts":[[2012,3,26]]},"assertion":[{"value":"2012-03-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}