Event-B to SMT-LIB: Difference between revisions
imported>Pascal |
imported>Pascal |
||
| Line 2: | Line 2: | ||
== Introduction == | == Introduction == | ||
The Event-B to [[#ancre_3|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 [[#ancre_1|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 == | == Specification == | ||
| Line 9: | Line 15: | ||
* <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> | ||
== User's Guide == | |||
== Bibliography == | == Bibliography == | ||
* <font id="ancre_1">DECERT</font>, [http://decert.gforge.inria.fr/index.html ''DEduction and CERTification''] | * <font id="ancre_1">DECERT</font>, [http://decert.gforge.inria.fr/index.html ''DEduction and CERTification''] | ||
* C. Pascal, [http://wiki.event-b.org/images/B2SMTLIB.pdf <font id="ancre_2">''From Event-B lemmas to SMT-LIB benchmarks''</font>, May 2009. | * C. Pascal, [http://wiki.event-b.org/images/B2SMTLIB.pdf <font id="ancre_2">''From Event-B lemmas to SMT-LIB benchmarks''</font>, May 2009. | ||
* S. Ranise and C. Tinelli, [http://goedel.cs.uiowa.edu/smtlib/papers/format-v1.2-r06.08.30.pdf <font id="ancre_3">''The SMT-LIB standard''</font>], Version 1.2, 2006, 2006. | |||
[[Category:Design]] | [[Category:Design]] | ||
Revision as of 08:31, 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
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, [http://wiki.event-b.org/images/B2SMTLIB.pdf From Event-B lemmas to SMT-LIB benchmarks, May 2009.
- S. Ranise and C. Tinelli, The SMT-LIB standard, Version 1.2, 2006, 2006.
