Dyna mite

Dynamite is a verification tool that extends PVS (Prototype Verification System) to provide comprehensive analysis of Alloy models.

It bridges the gap between the Alloy Analyzer's partial automatic verification and formal theorem proving, enabling semi-automatic verification for critical applications that require conclusive results.

• Dynamite: A Tool for the Verification of Alloy Models Based on PVSTOSEM 2014
• Improvements to Interactive Theorem Proving of Alloy Properties Using SAT-Solving (PhD thesis)2013
• Dynamite 2.0: New Features Based on UnSAT-Core Extraction to Improve Verification of Software RequirementsICTAC 2010
• Lessons Learned on the Verification of Models Using DynamiteAPV 2009
• Alloy Analyzer + PVS in the Analysis and Verification of Alloy SpecificationsTACAS 2007

Available for Linux, once the dependencies are installed.

1. Install the required software.
2. Download Dynamite with the button below.
3. Extract the files; this creates the DPSPATH directory.
4. Edit the DPS main script and set the four path variables: JAVAPATH, DPSPATH, PVSPATH, ALLOYPATH.

Questions about Dynamite? Copy Mariano Moscato's email address, or send your question with this form.