The probabilistic model checker Storm

Christian Hensel, Sebastian Junges, Joost Pieter Katoen*, Tim Quatmann, Matthias Volk

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

28 Citations (Scopus)
8 Downloads (Pure)


We present the probabilistic model checker Storm. Storm supports the analysis of discrete- and continuous-time variants of both Markov chains and Markov decision processes. Storm has three major distinguishing features. It supports multiple input languages for Markov models, including the Jani and Prism modeling languages, dynamic fault trees, generalized stochastic Petri nets, and the probabilistic guarded command language. It has a modular setup in which solvers and symbolic engines can easily be exchanged. Its Python API allows for rapid prototyping by encapsulating Storm’s fast and scalable algorithms. This paper reports on the main features of Storm and explains how to effectively use them. A description is provided of the main distinguishing functionalities of Storm. Finally, an empirical evaluation of different configurations of Storm on the QComp 2019 benchmark set is presented.

Original languageEnglish
Pages (from-to)589-610
Number of pages22
JournalInternational journal on software tools for technology transfer
Issue number4
Early online date6 Jul 2021
Publication statusPublished - Aug 2022
Externally publishedYes


  • Markov chain
  • Markov decision process
  • Model checking
  • Probilistic systems
  • Verification

Cite this