Dynamite

Automatic analysis of Alloy models is supported by the Alloy Analyzer, a tool that translates an Alloy model to a propositional formula that is then analyzed using off-the-shelf SAT solvers. The translation requires user-provided bounds on the sizes of data domains. The analysis is limited by the bounds and is therefore partial. Thus, the Alloy Analyzer may not be appropriate for the analysis of critical applications where more conclusive results are necessary. Dynamite is an extension of PVS that embeds a complete calculus for Alloy. It also includes extensions to PVS that allow one to improve the proof effort by, for instance, automatically analyzing new hypotheses with the aid of the Alloy Analyzer. Since PVS sequents may get cluttered with unnecessary formulas, we use the Alloy unsat-core extraction feature in order to refine proof sequents. An internalization of Alloy's syntax as an Alloy specification allows us to use the Alloy Analyzer for producing witnesses for proving existentially quantified formulas. Dynamite complements the partial automatic analysis offered by the Alloy Analyzer with semi-automatic verification through theorem proving. It also improves the theorem proving experience by using the Alloy Analyzer for early error detection, sequent refinement, and witness generation.

Platform Availability

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

System Requirements

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

1. Java 6.0 or above.
2. PVS 6.0 (on Emacs23 or above).
3. Alloy Analyzer 4.1.10

How to

1. Install required software.
2. Download Dynamite using the buton below.
3. Extract the contents of that file. A new directory will be created, containing the Dynamite Proving System. This will be the Dynamite directory (DPSPATH).
4. Edit the DPS main script (DPSPATH/dps), by modifying the value of the following constants:
   1. 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
   2. 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
   3. 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
   4. 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