www.prismmodelchecker.org

Download PRISM

PRISM is free and open source software. You can download both the tool and its source code for free from below. Distribution is under the GNU General Public License (GPL), version 2.


Latest version: 4.6

The current version of PRISM is 4.6 (first released 21 Apr 2020). The main changes since the last public release (4.5) are listed below. More details for individual releases are in the CHANGELOG.

  • New model checking features/enhancements:
    • digital clocks engine now supports time-bounded reachability
    • explicit engine support for steady-state computation (and S, R[S] properties)
    • improved support in MTBDD engine for very large (>2^63) state spaces
    • the -heuristic switch triggers automatic selection of some engines/settings
    • the -prop switch accepts multiple (comma-separated) property indices/names
    • MTBDD engine support for non-sparse vector printing (printall filter)
    • many minor bugfixes
  • New import/export features:
    • export of result values for all states of a model (-exportvector)
    • basic auto-detection of model type for explicit file import
    • simulation (path generation and statistical model checking) for explicit model imports
    • explicit engine support for state reward import from files
    • MTBDD engine support for export of transient/steady-state probabilities
  • Examples directory tidied up and now grouped by model type
  • Development changes and enhancements:
    • extended/improved ModelGenerator interface, including methods to support simulation
    • new RewardGenerator interface for specifying information about rewards for a model
    • PRISM API improvements: properties can be parsed against the currently loaded model
    • Makefile improvements: better configurability of directiories
    • Makefile improvements: better handling of variables and sub-Makefiles, incl. CUDD
    • new release_source Makefile target for building source releases
  • Benchmarking/testing changes and enhancements:
    • new prism-log-extract script for processing PRISM log files
    • prism-auto: new options/features (--log-subdirs, --filter-models, --args-list)

To access more recently developed features, get the latest code from GitHub.


Download:

PRISM should run on 32/64-bit versions of all major operating systems. We distribute pre-built binary versions for various architectures. But for non-Windows platforms, it is usually easy to build from source code.

Note: Your version (32- vs 64-bit) of Java must match that of PRISM. In particular, to use the 32-bit Windows binary, make sure you are running a 32-bit version of Java.

Please select a distribution:
Current release (4.6):
Source code
Windows (64-bit) installer
Linux (64-bit) binary
Mac OS X (64-bit) binary
Previous release (4.5):
Source code
Windows (32-bit) installer
Windows (64-bit) installer
Linux (64-bit) binary
Mac OS X (64-bit) binary
Name:
Affiliation: (e.g. name of university/company)
Email address (optional):

Where did you hear about PRISM?  


Installation

See the installation instructions, included in the PRISM manual (which is also distributed with the tool).

If you have any problems, first check the list of common problems and questions.

If you are still stuck, post a message in the forum.

Once you have installed PRISM, you might want to look at:

Downloads


76,027 downloads of PRISM to date.