SMT solvers for Rodin

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.
Type de document :
Communication dans un congrès
John Derrick and John A. Fitzgerald and Stefania Gnesi and Sarfraz Khurshid and Michael Leuschel and Steve Reeves and Elvinia Riccobene. ABZ - Third International Conference on Abstract State Machines, Alloy, B, VDM, and Z - 2012, Jun 2012, Pisa, Italy. Springer, 7316, pp.194-207, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-30885-7_14〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00747269
Contributeur : Pascal Fontaine <>
Soumis le : mardi 30 octobre 2012 - 21:53:42
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13

Identifiants

Collections

Citation

David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin. SMT solvers for Rodin. John Derrick and John A. Fitzgerald and Stefania Gnesi and Sarfraz Khurshid and Michael Leuschel and Steve Reeves and Elvinia Riccobene. ABZ - Third International Conference on Abstract State Machines, Alloy, B, VDM, and Z - 2012, Jun 2012, Pisa, Italy. Springer, 7316, pp.194-207, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-30885-7_14〉. 〈hal-00747269〉

Partager

Métriques

Consultations de la notice

225