PRISM People

Many people have contributed to the develoment of PRISM. Below is a (non-exhaustive) list of those who have worked on the tool itself or extensions to it. Apologies to anyone who we have omitted. Please contact us if this the case.

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.

PRISM development

The core team behind the development of PRISM, previously working in the School of Computer Science at the University of Birmingham and now working in the Computing Laboratory at the University of Oxford, comprises:

• Marta Kwiatkowska
• Gethin Norman
• Dave Parker
• Mark Kattenbelt

Contributions to the development of PRISM have also been gratefully received from:

• Andrew Hinton: Original versions of the GUI, Windows-port and simulator
• Joachim Meyer-Kayser: Implementation of the "Fox-Glynn" algorithm
• Alistair John Strachan: Port to 64-bit architectures
• Stephen Gilmore: Support for the stochastic process algebra PEPA
• Paolo Ballarini & Kenneth Chan: Port of PRISM to Mac OS X
• Rashid Mehmood: Improvements to low-level data structures and numerical solution algorithms
• Alistair John Strachan, Mike Arthur and Zak Cohen: Integration of JFreeChart into PRISM

The following people have collaborated on developing the theory behind PRISM and/or its case studies:

• Christel Baier: Model checking algorithms for probabilistic systems, see e.g. [BK98, Bai98, BCHG+97]
• Luca de Alfaro: Symbolic model checking techniques for MDPs [dAKN+00, BCHG+97]
• Joost-Pieter Katoen: CSL model checking algorithms [KKNP01]
• Antonio Pacheco: Extension of CSL model checking to allow the use of random time bounds, see [KNP05a, KNP02c, KNP02d]
• Roberto Segala: Model checking algorithms for probabilistic real-time automata and techniques for the analysis of distributed randomised algorithms, see [KNSS02, KNS01a, dAKN+00]
• Jeremy Sproston: Model checking algorithms for probabilistic real-time automata (applied to e.g. IEEE 1394 FireWire root contention and IEEE 802.11 Wireless LANs, see e.g. [KNS02a, KNS03b]

Extensions to PRISM

The following people are/were working on extensions and links to PRISM:

• Husain Aljazzar: Application of heuristic search algorithms to probabilistic model checking using PRISM's discrete event simulation engine.
  
• 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 [Gol04].
  
• 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.
  
• 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].
  
• Rashid Mehmood: Disk-based ("out-of-core") techniques. See these publications: [Meh04b, KPZM04, KMNP02, KM02]. Source code is available here.