{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,20]],"date-time":"2026-04-20T10:06:53Z","timestamp":1776679613070,"version":"3.51.2"},"reference-count":21,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012,6]]},"DOI":"10.1109\/topi.2012.6229810","type":"proceedings-article","created":{"date-parts":[[2012,7,10]],"date-time":"2012-07-10T17:36:12Z","timestamp":1341941772000},"page":"49-54","source":"Crossref","is-referenced-by-count":5,"title":["The EventB2Dafny Rodin plug-in"],"prefix":"10.1109","author":[{"given":"Nestor","family":"Catano","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K. Rustan M.","family":"Leino","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Victor","family":"Rivera","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","author":"fillia?tre","year":"2003","journal-title":"Why A Multi-language Multi-prover Verification Tool"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.03.007"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30885-7_17"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1145\/2245276.2231978"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1109\/CSD.2003.1207718"},{"key":"13","first-page":"259","article-title":"Matelas: A predicate calculus common formal definition for social networking","volume":"5977","author":"catan?o","year":"2010","journal-title":"LNCS"},{"key":"14","author":"owre","year":"2006","journal-title":"PVS Language Reference"},{"key":"11","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","article-title":"Rodin: An open toolset for modelling and reasoning in Event-B","volume":"12","author":"abrial","year":"2010","journal-title":"Software Tools for Technology Transfer"},{"key":"12","author":"catan?o","year":"2012","journal-title":"The EventB2Dafny Tool"},{"key":"21","first-page":"26","article-title":"Chase: A static checker for JML's assignable clause","volume":"2575","author":"catan?o","year":"2003","journal-title":"LNCS"},{"key":"3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1127878.1127884","article-title":"Preliminary design of JML: A behavioral interface specification language for Java","volume":"31","author":"leavens","year":"2006","journal-title":"ACM SIGSOFT"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_21"},{"key":"2","article-title":"Object Oriented Software Construction","author":"meyer","year":"1998","journal-title":"Series in Computer Science"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"10","first-page":"337","article-title":"Z3: An efficient SMT solver","volume":"4963","author":"de moura","year":"2008","journal-title":"LNCS"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"6","first-page":"348","article-title":"Dafny: An automatic program verifier for functional correctness","volume":"6355","author":"leino","year":"2010","journal-title":"LNCS"},{"key":"5","first-page":"49","article-title":"The Spec# programming system: An overview","volume":"3362","author":"barnett","year":"2005","journal-title":"LNCS"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.05.011"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_26"},{"key":"8","first-page":"364","article-title":"Boogie: A modular reusable verifier for object-oriented programs","volume":"4111","author":"barnett","year":"2006","journal-title":"LNCS"}],"event":{"name":"2012 2nd Workshop on Developing Tools as Plug-ins (TOPI)","location":"Zurich, Switzerland","start":{"date-parts":[[2012,6,3]]},"end":{"date-parts":[[2012,6,3]]}},"container-title":["2012 Second International Workshop on Developing Tools as Plug-Ins (TOPI)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/6220301\/6229799\/06229810.pdf?arnumber=6229810","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,20]],"date-time":"2017-06-20T17:11:13Z","timestamp":1497978673000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6229810\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6]]},"references-count":21,"URL":"https:\/\/doi.org\/10.1109\/topi.2012.6229810","relation":{},"subject":[],"published":{"date-parts":[[2012,6]]}}}