Event-B to SMT-LIB: Difference between revisions
imported>Pascal |
imported>Pascal |
||
| Line 16: | Line 16: | ||
* <tt>_exploratory/carinepascal/fr.systerel.decert</tt> | * <tt>_exploratory/carinepascal/fr.systerel.decert</tt> | ||
* <tt>_exploratory/carinepascal/fr.systerel.decert.tests</tt> | * <tt>_exploratory/carinepascal/fr.systerel.decert.tests</tt> | ||
The following theories are currently supported: Linear Arithmetic, Linear Order Int and Integer. | |||
== User's Guide == | == User's Guide == | ||
Revision as of 08:43, 25 August 2009
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
A first specification draft has been written.
Implementation
A first plug-in prototype is accessible under the following respositories:
- _exploratory/carinepascal/fr.systerel.decert
- _exploratory/carinepascal/fr.systerel.decert.tests
The following theories are currently supported: Linear Arithmetic, Linear Order Int and Integer.
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.
