creators_name: Déharbe, David creators_name: Fontaine, Pascal creators_name: Guyot, Yoann creators_name: Voisin, Laurent creators_id: david@dimap.ufrn.br creators_id: Pascal.Fontaine@inria.fr creators_id: yoann.guyot@systerel.fr creators_id: laurent.voisin@systerel.fr type: conference_item datestamp: 2012-07-18 12:48:03 lastmod: 2012-09-11 18:38:26 metadata_visibility: show title: SMT Solvers for Rodin ispublished: pub subjects: ADVANCE subjects: Event-Bsemantics subjects: Proof subjects: deploy_tooldev_rodinplugins full_text_status: public pres_type: paper abstract: Formal development in Event-B generally requires the validation of a large number of proof obligations. Some automatic tools exist to automatically discharge a significant part of them, thus augmenting the efficiency of the formal development. We here investigate the use of SMT (Satisfiability Modulo Theories) solvers in addition to the traditional tools, and detail the techniques used for the cooperation between the Rodin platform and SMT solvers. Our contribution is the definition of two approaches to use SMT solvers, their implementation in a Rodin plug-in, and an experimental evaluation on a large sample of industrial and academic projects. Adding SMT solvers to Atelier B provers reduces to one fourth the number of sequents that need to be proved interactively. date: 2012 date_type: published publication: ABZ 2012 volume: 7316 publisher: Springer Verlag pagerange: 194-207 event_title: ABZ 2012 event_location: Pisa, Italy event_dates: 19-21 June 2012 event_type: conference id_number: 10.1007/978-3-642-30885-7_14 refereed: TRUE issn: 0302-9743 official_url: http://dx.doi.org/10.1007/978-3-642-30885-7_14 citation: Déharbe, David and Fontaine, Pascal and Guyot, Yoann and Voisin, Laurent (2012) SMT Solvers for Rodin. In: ABZ 2012, 19-21 June 2012, Pisa, Italy. document_url: http://deploy-eprints.ecs.soton.ac.uk/424/1/73160194.pdf