Industrial deployment of system engineering methods providing high dependability and productivity


SMT Solvers for Rodin

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.

PDF - Accepted Version

Official URL:


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.

Item Type:Conference or Workshop Item (Paper)
Subjects:ADVANCE Project
Tool developments > Provers
Tool developments > Rodin plug-ins
ID Code:424
Deposited By: Laurent Voisin Laurent Voisin
Deposited On:18 Jul 2012 12:48
Last Modified:11 Sep 2012 18:38

Repository Staff Only: item control page

Deploy-Project - All right reserved