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 and CSL
  • Expected Rewards
  • Long-run Average Rewards
  • Conditional Probabilities
  • Multi-objective Model Checking


28 October 2021

QComp 2020 Results

Storm successfully participated in the second edition of the Comparison of Tools for the Analysis of Quantitative Formal Models (QComp 2020). The competition report is available here.

15 May 2021

Storm in Aachener Nachrichten

The newspaper Aachener Nachrichten published the article Storm findet sicherheitskritische Softwarefehler.

05 March 2021

2nd place at RWTH Innovation Award 2020

The Storm model checker has received the second place at the RWTH Innovation Award 2020. The annual awards honours ideas and technologies developed by researchers and inventors at RWTH Aachen University.