Difference between revisions of "SMT Solvers Plug-in"
From Event-B
Jump to navigationJump to searchimported>Fages |
imported>Fages |
||
| Line 2: | Line 2: | ||
The SMT plug-in allows to use SMT solvers within Rodin. | The SMT plug-in allows to use SMT solvers within Rodin. | ||
| + | For the moment, it can handle some basic arithmetic proof obligations but still needs to be improved to be much more efficient. | ||
== Usage == | == Usage == | ||
Revision as of 15:04, 24 September 2010
Introduction
The SMT plug-in allows to use SMT solvers within Rodin.
For the moment, it can handle some basic arithmetic proof obligations but still needs to be improved to be much more efficient.
