Dynamite Proving System

News

Dynamite 2.0 is now available
See section "Download & Installation" for installations details.
In section Examples you will find elaborated examples of the use of Dynamite (including proofs of assertions in Zave's work: Compositional Binding in Network Domains).

Install required software (see System Requirements).
Download Dynamite from here.
Extract the contents of that file. A new directory will be created, containing the Dynamite Proving System. This will be the Dynamite directory (DPSPATH).
Edit the DPS main script (DPSPATH/dps), by modifying the value of the following constants:
- JAVAPATH: full path to the java virtual machine.
  For instance, if your JVM is located inside directory /usr/lib/jvm/default-java/bin, the third line of the script should read JAVAPATH=/usr/lib/jvm/default-java/bin
- DPSPATH: full path of the Dynamite directory.
  If you have installed Dynamite in the directory /opt/dps, the corresponding line should read DPSPATH=/opt/dps
- PVSPATH: full path of the PVS directory.
  If PVS is installed in your system in directory /opt/pvs, the PVSPATH variable should contain that value, ie, PVSPATH=/opt/pvs
- ALLOYPATH: full path of the Alloy directory.
  If the Alloy jar is located in directory /opt/alloy4, the last variable definition of the script should read ALLOYPATH=/opt/alloy4

The current version of the system is 0.2.3 (a.k.a Dynamite 2.0).

This is an alpha version. Please report any bug you find to Mariano M. Moscato.

The Dynamite Proving system is available for any Linux platform all its software requirements are available (see System Requirements).

To run the Dynamite Proving System the following software must be installed:

A brief tutorial can be found here.

A list of known bugs and limitations can be found here.

A brief description of the Dynamite main commands can be found here.

A list of known installation troubles is reported here.

The Dynamite To-Do list can be consulted here.