www.prismmodelchecker.org

PRISM - People

PRISM was created and is still actively maintained by:

Development of the tool is currently led from Oxford by Dave Parker.

The following have made a wide range of contributions to PRISM covering many different aspects of the tool (in approximately reverse chronological order):

We also gratefully acknowledge contributions to the PRISM code-base from (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.

  • Husain Aljazzar: Application of heuristic search algorithms to probabilistic model checking using PRISM's discrete event simulation engine.
  • Radu Calinescu: PRISM-driven online adaptation in self-* systems [CK09, CK09b].
  • Conrado Daws: Techniques to model check probabilistic real-time automata with PRISM, in conjunction with the real-time model checker KRONOS. 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].
  • Matthias Kuntz, Markus Siegle and Edith Werner: Integration of PRISM numerical solution engines into the tool CASPA. See [KSW04b].
  • Formal Systems: An interface between PRISM and FDR2. This will allow PRISM to work with with CSP models. See [GW05].
  • Thomas Hérault and Sylvain Peyronnet: Integration into PRISM of techniques from the tool APMC, which performs approximate verification of probabilistic systems using a Monte-Carlo algorithm.
  • Pascal Honoré: 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.
  • Vivien Maisonneuve: Automatic heuristic-based generation of MTBDD variable orderings for PRISM models.
  • Rashid Mehmood: Disk-based ("out-of-core") techniques. See these publications: [Meh04b, KPZM04, KMNP02, KM02]. Source code is available here.
  • Fuzhi Wang: Efficient symbolic data structures for model checking of probabilistic timed automata. See here for some preliminary results.
  • Håkan Younes: Comparison of PRISM with sampling-based techniques for probabilistic verification of discrete event systems. See the publication [YKNP05] and the tools ProVer and Ymer.
  • Yi Zhang: PRISM numerical solution engines for parallel/distributed/Grid computing. See [ZPK05a, ZPK05b, KPZM04].

See also here for publications about extensions and connections to PRISM.

About PRISM