SMT solvers for Rodin

David Déharbe 1 Pascal Fontaine 2 Yoann Guyot 3 Laurent Voisin 3
2 VERIDIS - VERIfication pour les systèmes DIStribués
Inria Nancy - Grand Est, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications : UMR7503
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.
Document type :
Conference papers
Liste complète des métadonnées
Contributor : Pascal Fontaine <>
Submitted on : Tuesday, October 30, 2012 - 9:53:42 PM
Last modification on : Thursday, February 21, 2019 - 2:02:02 PM




David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin. SMT solvers for Rodin. ABZ - Third International Conference on Abstract State Machines, Alloy, B, VDM, and Z - 2012, Jun 2012, Pisa, Italy. pp.194-207, ⟨10.1007/978-3-642-30885-7_14⟩. ⟨hal-00747269⟩



Record views