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.4

The current version of PRISM is 4.4 (first released 23 Jul 2017). The main changes since the last public release (4.3.1) are listed below. More details for individual releases are in the CHANGELOG.

  • New model checking functionality:
    • expected reward to satisfy a co-safe LTL formula (MDPs, D/CTMCs, all engines)
    • interval iteration (MDPs, D/CTMCs, all engines)
    • topological value iteration (MDPs, D/CTMCs, explicit engine)
    • expected total reward (R[C] operator) for CTMCs and MDPs (max), all engines
    • CTL model checking in the explicit engine
    • non-probabilistic LTL model checking in the explicit engine
    • instantaneous reward computation (Rmax/min[I=x]) in the explicit engine
    • DTMC transient probability computation for the explicit engine
  • Imports and exports:
    • model import from explicit files for the explicit engine (-import... switches)
    • full import of labels during explicit model import (all engines)
    • import of state rewards during explicit model import (symbolic engines)
    • export of state rewards from explicit engine
    • export of models to .dot format via the -exportmodel switch
  • Miscellaneous:
    • built-in support for Nailgun client/server
    • new timeout feature (-timeout switch)
    • performance improvements in explicit engine
    • GUI also supports -javamaxmem switch to set Java memory
    • better error handling when CUDD runs out of memory
    • various bug fixes and performance improvements
  • Features for developers:
    • new ModelGenerator interface for specifying models programmatically
    • extensions to test mode: complex expressions for RESULT specifications
    • prism-auto: new options/features (e.g., --show-warnings, --nailgun, --ngprism, --verbose-test)
    • DD debugging options: -dddebug and -ddtrace switches, improved ref count debugging
    • new option -exportiterations for visualising iterative numerical methods
    • code base now allows/assumes Java 8

To access more recently developed features, try the development versions, or check 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.4.beta):
Source code
Windows (32-bit) installer
Windows (64-bit) installer
Linux (32-bit) binary
Linux (64-bit) binary
Mac OS X (32-bit) binary
Mac OS X (64-bit) binary
Previous release (4.3.1):
Source code
Windows (32-bit) installer
Windows (64-bit) installer
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


62,632 downloads of PRISM to date.