Storm is a tool for the analysis of systems involving random or probabilistic phenomena. Given an input model and a quantitative specification, it can determine whether the input model conforms to the specification. It has been designed with performance and modularity in mind.

Modeling formalisms

Storm is built around discrete- and continuous-time Markov models:
  • Discrete Time Markov Chains
  • Markov Decision Processes
  • Continuous Time Markov Chains
  • Markov Automata

Input languages

Storm supports several types of input:
  • JANI
  • GSPNs
  • DFTs
  • cpGCL
  • explicit


Storm focuses on reachability queries and its support includes
  • PCTL
  • CSL
  • Expected Rewards
  • Conditional Probabilities


18 June 2020

Videos of Storm tutorial

The videos of our Storm tutorial are available on YouTube.

15 June 2020

Storm tutorial at DisCoTec 2020

We are giving an (online) tutorial on Storm at DisCoTec 2020.

08 June 2020

New version 1.6.0

We are happy to announce the next stable releases of Storm and stormpy in version 1.6.0.