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.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{DeharbeFGV12,
author = {David D{\'{e}}harbe and
Pascal Fontaine and
Yoann Guyot and
Laurent Voisin},
editor = {John Derrick and
John S. Fitzgerald and
Stefania Gnesi and
Sarfraz Khurshid and
Michael Leuschel and
Steve Reeves and
Elvinia Riccobene},
title = {{SMT} Solvers for Rodin},
booktitle = {Abstract State Machines, Alloy, B, VDM, and {Z} - Third International
Conference, {ABZ} 2012, Pisa, Italy, June 18-21, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7316},
pages = {194--207},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-30885-7\_14},
doi = {10.1007/978-3-642-30885-7\_14},
timestamp = {Sun, 02 Jun 2019 21:23:59 +0200},
biburl = {https://dblp.org/rec/conf/asm/DeharbeFGV12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}