  We launch the new probabilistic model checker storm. It features the analysis
of discrete- and continuous-time variants of both Markov chains and MDPs. It
supports the PRISM and JANI modeling languages, probabilistic programs, dynamic
fault trees and generalized stochastic Petri nets. It has a modular set-up in
which solvers and symbolic engines can easily be exchanged. It offers a Python
API for rapid prototyping by encapsulating storm's fast and scalable
algorithms. Experiments on a variety of benchmarks show its competitive
performance.
