Pith. sign in

REVIEW 2 cited by

The Probabilistic Model Checker Storm

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2002.07080 v2 pith:2KRDF7FY submitted 2020-02-17 cs.SE

Christian Hensel , Sebastian Junges , Joost-Pieter Katoen , Tim Quatmann , Matthias Volk This is my paper · ORCID
classification cs.SE
keywords stormmarkovprobabilisticcheckerdistinguishingfeatureslanguagesmain
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

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 set-up 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.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. A Fast Quantitative Analyzer for NetKAT

    cs.PL 2026-07 conditional novelty 8.0 of 10

    wSPPs compactly compute weighted NetKAT semantics over any semiring, including Kleene star, and trace-carrying Pareto semirings add witness paths for multi-objective trade-offs.

  2. Towards Unified Probabilistic Verification and Validation of Vision-Based Autonomy

    eess.SY 2025-08 reject novelty 5.0 of 10

    A pipeline that turns collected runs of a vision-based controller into an interval MDP, verifies a safety lower bound, and reuses Bayesian conformance to extend the bound to new environments.

Pith tools