Design Environments
ESPRIT Framework IV LTR 26241
Plugins
|
A number of plug-in verification components are being developed by the PROSPER project and by third parties. Some of these work by adding the PROSPER Integration Interface to the verification component. This is the recommended approach to building a PROSPER plugin. However, where access to the source code of the component is not available, other means have been used to construct a plugin. In both cases the plugin appears to a proof engine as an Application Programming Interface (API). Except where otherwise stated, contact Glasgow for details of the existing plugins. |
| Official PROSPER Plugins |
| BuDDy BDD package |
The BuDDy Binary Decision Diagram package comes as a module with HOL98, which is in turn used to build the PROSPER Core Proof Engine. The code for turning BuDDy into a plugin is bundled with the PROSPER Toolkit. |
| A plugin using Prover |
This plugin implements a propositional logic decision procedure based on Stålmarck's Method. It is a commercial product marketed by Prover Technology, one of the PROSPER project partners. Contact Lars Lundgren for more information. |
| SMV plugin |
This plugin is based on the SMV model checker. The code to turn SMV into a plugin is bundled with the PROSPER Toolkit but it is a prototype and we cannot guarantee that it is compatible with the current version of SMV. A description of the plugin can be found on the deliverables page. |
| Third-Party Plugins |
Plugins based on ACL2, SVC, and Gandalf have been developed by third parties. |