PRISM - People
PRISM was created and is still actively maintained by:
Development of the tool is currently led from Birmingham
by Dave Parker.
Several of the other people actively developing PRISM and its extensions are based in
We gratefully acknowledge contributions to the PRISM code-base from various sources,
including (in approximately reverse chronological order):
See also here for details of third-party tools/libraries included in PRISM.
Details of the people who worked on the underlying theory and techniques implemented in PRISM
can be found here.
There are also many people who have worked on case studies using PRISM.
You can find details of these in the case studies section of the site.
Extensions to PRISM
The following is a (non-exhaustive) list of people who are/were working on extensions and links to PRISM.
Apologies to anyone who we have omitted. Please contact us if this the case.
Application of heuristic search algorithms to probabilistic model checking
using PRISM's discrete event simulation engine.
PRISM-driven online adaptation in self-* systems [CK09, CK09b].
Techniques to model check probabilistic real-time automata with PRISM,
in conjunction with the real-time model checker
This approach has been used to analyse the IEEE 1394 FireWire root contention protocol.
More information can be found here
and in the following publication: [DKN04].
Alastair Donaldson and Alice Miller:
The tool GRIP: a symmetry reduction tool for PRISM;
see also [DMP07, DM06].
Markus Siegle and
Integration of PRISM numerical solution engines into the tool CASPA.
An interface between PRISM and
This will allow PRISM to work with with CSP models.
Thomas Hérault and
Integration into PRISM of techniques from the tool APMC,
which performs approximate verification of probabilistic systems using a Monte-Carlo algorithm.
Extensions/adaptions of PRISM for the analysis of mobile systems.
Tran Manh Ha Tran:
Ports of PRISM to 64-bit architectures and investigation into parallelisation.
Automatic heuristic-based generation of MTBDD variable orderings for PRISM models.
Disk-based ("out-of-core") techniques. See these publications: [Meh04b, KPZM04, KMNP02, KM02].
Source code is available here.
Efficient symbolic data structures for model checking of probabilistic timed automata.
See here for some preliminary results.
Comparison of PRISM with sampling-based techniques for probabilistic verification of discrete event systems.
See the publication [YKNP05] and the tools
PRISM numerical solution engines for parallel/distributed/Grid computing.
See [ZPK05a, ZPK05b, KPZM04].
See also here for publications about extensions and connections to PRISM.