PRISM is a tool for formally verifying the correctness of probabilistic systems.

PRISM is a software tool for modelling and studying the behaviour of real-life systems whose behaviour exhibits unpredictability or randomness. It can be used to analyse everything from the reliability of distributed file systems, to the performance of a Bluetooth-enabled wireless device, to the safety of a car's airbag control system. PRISM has been used by researchers worldwide in fields as diverse as quantum cryptography, systems biology, computer security and robotics. Development of PRISM is based at the University of Birmingham and the University of Oxford, UK, but we have contributors worldwide. It has been under development for over 10 years and contains about 200K lines of code in total. The software is coded primarily in Java, including a graphical user interface written in Swing, but with various underlying libraries written in C/C++.

lightbulb_outline View ideas list


  • java
  • c++


email Mailing list
mail_outline Contact email

PRISM Model Checker 2016 Projects

  • Muhammad Omer Saeed
    Enhanced Graph Plotting and General GUI Improvements in Prism
    Prism is a tool for probabilistic model checking. It is categorized as a formal verification system tool for the modelling and analysis of systems...
  • Ganindu
    Enhanced Strategy Functionality for PRISM
    Prism is a probabilistic model checker, by which, the users can model and analyse real time systems. Prism provides its own modelling language. A...
  • Nicolas Del Piano
    Exact Solution Methods
    Nowadays, most floating point computations are performed in double precision – with a mantissa of 53 bits. Nevertheless, depending on the application...
  • christopherZ
    Extended support for mean-payoff properties
    In this project the multi-objective mean-payoff properties in Markov decision process are to be added into Prism, which is a probabilistic model...
  • Maximilian Probst
    Refactoring and optimizing model construction for the explicit engine
    During the project the current model construction will be analysed in regard to performance(i.e. reachability of multiple initial states, scalability...