PV3 Stormcomputes how a given property is related to a given specification

Application domain/field

Type of tool

Probabilistic model checker

Expected input


Storm supports many different input formats:

Expected output

Depends on the property. It can give the probability of a certain outcome, but also whether a property is true or false. It will also give information about the model such as the number of states and transitions.


It uses the following solvers: Eigen, gmm++, CUDD, Sylvan, Gurobi, GLPK, Z3, MathSAT, SMT-LIB


There is also a fuzzer that is called STORM.
Model checking Probabilistic


Related papers

Last publication date

6 July 2021

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.