Event-B to SMT-LIB
Introduction
The Event-B to SMT-LIB plug-in allows to translate mathematical lemmas that rely on the Event-B language to the SMT-LIB format.
The considered lemmas are those often encountered in practice, but not yet well supported by proving tools such as those embedded in the Rodin platform. The purpose is not here to entirely define the translation, but rather to give a mapping for this subset of Event-B formulas. These typical mathematical problems are entry points for the DECERT project, and more precisely for the Work Package 1. Using the SMT-LIB standard is among the requirements for this project.
This version mainly focuses on lemmas based on unquantified integer linear arithmetic.
Specification
Implementation
A first plug-in prototype is accessible under the following respositories:
- _exploratory/carinepascal/fr.systerel.decert
- _exploratory/carinepascal/fr.systerel.decert.tests
User's Guide
Bibliography
- DECERT, DEduction and CERTification
- C. Pascal, From Event-B lemmas to SMT-LIB benchmarks, May 2009.
- S. Ranise and C. Tinelli, The SMT-LIB standard, Version 1.2, 2006, 2006.
