--- 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.\r\n\r\nOur 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." accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: [] creators_id: - david@dimap.ufrn.br - Pascal.Fontaine@inria.fr - yoann.guyot@systerel.fr - laurent.voisin@systerel.fr creators_name: - family: Déharbe given: David honourific: '' lineage: '' - family: Fontaine given: Pascal honourific: '' lineage: '' - family: Guyot given: Yoann honourific: '' lineage: '' - family: Voisin given: Laurent honourific: '' lineage: '' data_type: ~ date: 2012 date_type: published datestamp: 2012-07-18 12:48:03 department: ~ dir: disk0/00/00/04/24 divisions: [] edit_lock_since: ~ edit_lock_until: 0 edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 424 event_dates: 19-21 June 2012 event_location: 'Pisa, Italy' event_title: ABZ 2012 event_type: conference exhibitors_id: [] exhibitors_name: [] fileinfo: /style/images/fileicons/application_pdf.png;/424/1/73160194.pdf full_text_status: public funders: [] id_number: 10.1007/978-3-642-30885-7_14 importid: ~ institution: ~ isbn: ~ ispublished: pub issn: 0302-9743 item_issues_comment: [] item_issues_count: ~ item_issues_description: [] item_issues_id: [] item_issues_reported_by: [] item_issues_resolved_by: [] item_issues_status: [] item_issues_timestamp: [] item_issues_type: [] keywords: ~ lastmod: 2012-09-11 18:38:26 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: ~ official_url: http://dx.doi.org/10.1007/978-3-642-30885-7_14 output_media: ~ pagerange: 194-207 pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: paper producers_id: [] producers_name: [] projects: - Decert - Deploy publication: ABZ 2012 publisher: Springer Verlag refereed: TRUE referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 13 series: ~ skill_areas: [] source: ~ status_changed: 2012-07-18 12:48:03 subjects: - ADVANCE - Event-Bsemantics - Proof - deploy_tooldev_rodinplugins succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: SMT Solvers for Rodin type: conference_item userid: 106 volume: 7316