Table of contents
Storm tool papers
If you want to cite Storm, please use the most recent paper in this category.
- Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk, “The probabilistic model checker Storm,” Int. J. Softw. Tools Technol. Transf., no. 4, 2022.
- Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk, “A Storm is Coming: A Modern Probabilistic Model Checker,” in CAV (2), 2017.
- Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk, “The Probabilistic Model Checker Storm (Extended Abstract),” CoRR, 2016.
Competition reports
The publications in this category present tool comparisons.
- Roman Andriushchenko et al., “Tools at the Frontiers of Quantitative Verification - QComp 2023 Competition Report,” TOOLympics@ETAPS, 2023.
- Carlos E. Budde et al., “On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report,” in ISoLA (4), 2020.
- Ernst Moritz Hahn et al., “The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report),” in TACAS (3), 2019.
Storm tutorials
The publications in this category present tutorials on Storm. See also the dedicated tutorial page.
- Matthias Volk, Linus Heck, Sebastian Junges, Joost-Pieter Katoen, and Tim Quatmann, “Probabilistic Model Checking Taken by Storm - A Tutorial on the Probabilistic Model Checker Storm,” in FM (2), 2026.
Papers about features in Storm
The publications in this category present functionality from which a substantial part is available in Storm’s release.
2026
- Arnd Hartmanns, Tim Quatmann, and Mark van Wijk, “Tools and Algorithms for Sound Multi-Objective Probabilistic Model Checking - (Long Tool Paper),” in FM (1), 2026.
- Julius Ide, Joost-Pieter Katoen, Hannah Mertens, and Tim Quatmann, “Multiple Long-Run and omega-Regular Objectives in MDPs,” in TACAS (1), 2026.
2025
- Alexander Bork, Joost-Pieter Katoen, Tim Quatmann, and Svenja Stein, “Multi-Cost-Bounded Reachability Analysis of POMDPs,” in UAI, 2025.
- Krishnendu Chatterjee, Mahdi JafariRaviz, Raimundo Saona, and Jakub Svoboda, “Value Iteration with Guessing for Markov Chains and Markov Decision Processes,” in TACAS (2), 2025.
- Krishnendu Chatterjee, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, and Daniel Zilken, “Fixed Point Certificates for Reachability and Expected Rewards in MDPs,” in TACAS (2), 2025.
- Linus Heck, Tim Quatmann, Jip Spel, Joost-Pieter Katoen, and Sebastian Junges, “Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains,” in ATVA, 2025.
- Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, and Tobias Winkler, “Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate,” J. Autom. Reason., no. 3, 2025.
- Tim Quatmann, “What is the best algorithm for MDP model checking?,” Int. J. Softw. Tools Technol. Transf., no. 4, 2025.
2024
- Sebastian Junges et al., “Parameter synthesis for Markov models: covering the parameter space,” Formal Methods Syst. Des., no. 1, 2024.
- Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, and Tobias Winkler, “Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains,” in TACAS (2), 2024.
2022
- Daniel Basgöze, Matthias Volk, Joost-Pieter Katoen, Shahid Khan, and Mariëlle Stoelinga, “BDDs Strike Back - Efficient Analysis of Static and Dynamic Fault Trees,” in NFM, 2022.
- Alexander Bork, Joost-Pieter Katoen, and Tim Quatmann, “Under-Approximating Expected Total Rewards in POMDPs,” in TACAS (2), 2022.
- Linus Heck, Jip Spel, Sebastian Junges, Joshua Moerman, and Joost-Pieter Katoen, “Gradient-Descent for Randomized Controllers Under Partial Observability,” in VMCAI, 2022.
- Tim Quatmann, Sebastian Junges, and Joost-Pieter Katoen, “Markov automata with multiple objectives,” Formal Methods Syst. Des., no. 1, 2022.
2021
- Sebastian Junges, Nils Jansen, and Sanjit A. Seshia, “Enforcing Almost-Sure Reachability in POMDPs,” in CAV (2), 2021.
- Tim Quatmann and Joost-Pieter Katoen, “Multi-objective Optimization of Long-run Average and Total Rewards,” in TACAS (1), 2021.
- Jip Spel, Sebastian Junges, and Joost-Pieter Katoen, “Finding Provably Optimal Markov Chains,” in TACAS, 2021.
2020
- Alexander Bork, Sebastian Junges, Joost-Pieter Katoen, and Tim Quatmann, “Verification of Indefinite-Horizon POMDPs,” in ATVA, 2020.
- Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann, and Mickael Randour, “Simple Strategies in Multi-Objective MDPs,” in TACAS (1), 2020.
- Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, and Tim Quatmann, “Multi-cost Bounded Tradeoff Analysis in MDP,” J. Autom. Reason., no. 7, 2020.
2018
- Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, and Tim Quatmann, “Multi-cost Bounded Reachability in MDP,” in TACAS (2), 2018.
- Sebastian Junges, Joost-Pieter Katoen, Mariëlle Stoelinga, and Matthias Volk, “One Net Fits All - A Unifying Semantics of Dynamic Fault Trees Using GSPNs,” in Petri Nets, 2018.
- Tim Quatmann and Joost-Pieter Katoen, “Sound Value Iteration,” in CAV (1), 2018.
- Matthias Volk, Sebastian Junges, and Joost-Pieter Katoen, “Fast Dynamic Fault Tree Analysis by Model Checking Techniques,” IEEE Trans. Ind. Informatics, no. 1, 2018.
2017
- Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn, Arnd Hartmanns, Sebastian Junges, and Andrea Turrini, “JANI: Quantitative Model and Tool Interaction,” in TACAS (2), 2017.
- Tim Quatmann, Sebastian Junges, and Joost-Pieter Katoen, “Markov Automata with Multiple Objectives,” in CAV (1), 2017.
2016
- Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu, and Joost-Pieter Katoen, “Safety-Constrained Reinforcement Learning for MDPs,” in TACAS, 2016.
- Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen, “Parameter Synthesis for Markov Models: Faster Than Ever,” in ATVA, 2016.
- Matthias Volk, Sebastian Junges, and Joost-Pieter Katoen, “Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates,” in SAFECOMP, 2016.
2015
- Christian Dehnert et al., “PROPhESY: A PRObabilistic ParamEter SYnthesis Tool,” in CAV (1), 2015.
2014
- Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, and Joost-Pieter Katoen, “Fast Debugging of PRISM Models,” in ATVA, 2014.
Tools using Storm
A list of tools which make use of Storm.
- Caesar: Deductive verifier for probabilistic programs
- CONVINCE: Open source toolbox to improve robust robot deliberation with the help of planning, learning, and model checking techniques
- COOL-MC: Combining single-agent and multi-agent reinforcement learning with model checking
- jajapy: Baum-Welch algorithm on various kinds of Markov models
- Momba: Python framework for dealing with quantitative models centered around the JANI-model interchange format
- Prophesy: Parameter synthesis in Markov models
- PAYNT: Automated synthesis of probabilistic programs
- QMaude: Quantitative specification and verification in Maude
- SAFEST: Dynamic fault-tree analysis tool
- STAMINA: State-space truncation tool that can analyze infinite-sized models
- TEMPEST: Synthesis tool for reactive systems and shields in probabilistic environments
Papers using Storm as a backend
The publications in this category present tools, algorithms and case studies that use Storm as a backend.
2026
- Roman Andriushchenko, Alexander Bork, Milan Ceska, Sebastian Junges, Joost-Pieter Katoen, and Filip Macák, “Search and Explore: Symbiotic Policy Synthesis in POMDPs,” Formal Methods Syst. Des., no. 1, 2026.
- Linus Heck, Filip Macák, Milan Ceska, and Sebastian Junges, “Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking,” in AAAI 2026, 2026.
- Antonina Skurka, Luko van der Maas, Sebastian Junges, and Hazem Torfah, “Learning Robust Markov Models for Safe Runtime Monitoring,” in AAMAS, 2026.
2025
- Suguman Bansal and Ramneet Singh, “INTERLEAVE: A Faster Symbolic Algorithm for Maximal End Component Decomposition,” in CAV (2), 2025.
- Luko van der Maas and Sebastian Junges, “Learning Verified Monitors for Hidden Markov Models,” in ATVA, 2025.
- Francesco Pontiggia, Filip Macák, Roman Andriushchenko, Michele Chiari, and Milan Ceska, “Decentralized Planning Using Probabilistic Hyperproperties,” in AAMAS, 2025.
2024
- Thom S. Badings, Matthias Volk, Sebastian Junges, Mariëlle Stoelinga, and Nils Jansen, “CTMCs with Imprecisely Timed Observations,” in TACAS (2), 2024.
- Alexander Bork, Debraj Chakraborty, Kush Grover, Kretı́nský Jan, and Stefanie Mohr, “Learning Explainable and Better Performing Representations of POMDP Strategies,” in TACAS (2), 2024.
- Tamme Emunds and Nils Nießen, “Evaluating railway junction infrastructure: A queueing-based, timetable-independent analysis,” Transportation Research Part C: Emerging Technologies, 2024.
- Christian Hensel, Sebastian Junges, Tim Quatmann, and Matthias Volk, “Riding the Storm in a Probabilistic Model Checking Landscape,” in Principles of Verification (2), 2024.
- Kazuki Watanabe, Marck van der Vegt, Sebastian Junges, and Ichiro Hasuo, “Compositional Value Iteration with Pareto Caching,” in CAV (3), 2024.
- Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo, Jurriaan Rot, and Sebastian Junges, “Pareto Curves for Compositionally Model Checking String Diagrams of MDPs,” in TACAS, 2024.
2023
- Steven Carr, Nils Jansen, Sebastian Junges, and Ufuk Topcu, “Safe Reinforcement Learning via Shielding under Partial Observability,” in AAAI, 2023.
- Arnd Hartmanns, Sebastian Junges, Tim Quatmann, and Maximilian Weininger, “A Practitioner’s Guide to MDP Model Checking Algorithms,” in TACAS, 2023.
- Joshua Jeppson et al., “STAMINA in C++: Modernizing an Infinite-State Probabilistic Model Checker,” in QEST, 2023.
- Marck van der Vegt, Nils Jansen, and Sebastian Junges, “Robust Almost-Sure Reachability in Multi-Environment MDPs,” in TACAS (1), 2023.
2022
- Thom S. Badings, Nils Jansen, Sebastian Junges, Mariëlle Stoelinga, and Matthias Volk, “Sampling-Based Verification of CTMCs with Uncertain Rates,” in CAV (2), 2022.
- Thom Badings, Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, and Ufuk Topcu, “Scenario-Based Verification of Uncertain Parametric MDPs,” STTT, 2022.
- Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, and Ufuk Topcu, “Convex Optimization for Parameter Synthesis in MDPs,” IEEE Trans. Autom. Control., 2022.
- Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen, “Parameter Synthesis in Markov Models: A Gentle Survey,” in Principles of Systems Design, 2022.
- Sebastian Junges and Matthijs T. J. Spaan, “Abstraction-Refinement for Hierarchical Probabilistic Models,” in CAV, 2022.
- Tatjana Petrov, Matej Hajnal, Julia Klein, David Safránek, and Morgane Nouvian, “Extracting individual characteristics from population data reveals a negative social effect during honeybee defence,” PLoS Comput. Biol., no. 9, 2022.
- Jip Spel, Svenja Stein, and Joost-Pieter Katoen, “POMDP Controllers with Optimal Budget,” in QEST, 2022.
- Matthias Volk, Borzoo Bonakdarpour, Joost-Pieter Katoen, and Saba Aflaki, “Synthesizing optimal bias in randomized self-stabilization,” Distributed Comput., no. 1, 2022.
- Norman Weik, Matthias Volk, Joost-Pieter Katoen, and Nils Nießen, “DFT modeling approach for operational risk assessment of railway infrastructure,” Int. J. Softw. Tools Technol. Transf., no. 3, 2022.
2021
- Milan Ceska, Christian Hensel, Sebastian Junges, and Joost-Pieter Katoen, “Counterexample-guided Inductive Synthesis for Probabilistic Systems,” Formal Asp. Comput., 2021.
- Murat Cubuktepe, Nils Jansen, Sebastian Junges, Ahmadreza Marandi, Marnix Suilen, and Ufuk Topcu, “Robust Finite-State Controllers for Uncertain POMDPs,” in AAAI, 2021.
- Arnd Hartmanns, Joost-Pieter Katoen, Bram Kohlen, and Jip Spel, “Tweaking the Odds in Probabilistic Timed Automata,” in QEST, 2021.
- Steven Holtzen, Sebastian Junges, Marcell Vazquez-Chanlatte, Todd D. Millstein, Sanjit A. Seshia, and Guy Van den Broeck, “Model Checking Finite-Horizon Markov Chains with Probabilistic Inference,” in CAV, 2021.
- Sebastian Junges, Hazem Torfah, and Sanjit A. Seshia, “Runtime Monitors for Markov Decision Processes,” in CAV, 2021.
- Shahid Khan, Joost-Pieter Katoen, Matthias Volk, and Marc Bouissou, “Scalable Reliability Analysis by Lazy Verification,” in NFM, 2021.
- Shahid Khan, Joost-Pieter Katoen, Matthias Volk, Muhammad Ahmad Zafar, and Falak Sher, “Modelling and Analysis of Fire Sprinklers by Verifying Dynamic Fault Trees,” in LADC, 2021.
- Shahid Khan, Matthias Volk, Joost-Pieter Katoen, Alexis Braibant, and Marc Bouissou, “Model Checking the Multi-Formalism Language FIGARO,” in DSN, 2021.
- Stefan Pranger, Bettina Könighofer, Lukas Posch, and Roderick Bloem, “TEMPEST - Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments,” in ATVA, 2021.
- Bahare Salmani and Joost-Pieter Katoen, “Fine-Tuning the Odds in Bayesian Networks,” in ECSQARU, 2021.
- Han Zhang, Chi Zhang, Arthur Azevedo de Amorim, Yuvraj Agarwal, Matt Fredrikson, and Limin Jia, “Netter: Probabilistic, Stateful Network Models,” in VMCAI, 2021.
2020
- Nils Jansen, Bettina Könighofer, Sebastian Junges, Alex Serban, and Roderick Bloem, “Safe Reinforcement Learning Using Probabilistic Shields (Invited Paper),” in CONCUR, 2020.
- Bahare Salmani and Joost-Pieter Katoen, “Bayesian Inference by Symbolic Model Checking,” in QEST, 2020.
2019
- Milan Ceska, Christian Hensel, Sebastian Junges, and Joost-Pieter Katoen, “Counterexample-Driven Synthesis for Probabilistic Program Sketches,” in FM, 2019.
- Milan Ceska, Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen, “Shepherding Hordes of Markov Chains,” in TACAS (2), 2019.
- Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, and Matthias Volk, “Safety analysis for vehicle guidance systems with dynamic fault trees,” Reliab. Eng. Syst. Saf., 2019.
- Arnd Hartmanns, Michaela Klauck, David Parker, Tim Quatmann, and Enno Ruijters, “The Quantitative Verification Benchmark Set,” in TACAS (1), 2019.
- Jip Spel, Sebastian Junges, and Joost-Pieter Katoen, “Are Parametric Markov Chains Monotonic?,” in ATVA, 2019.
- Matthias Volk, Norman Weik, Joost-Pieter Katoen, and Nils Nießen, “A DFT Modeling Approach for Infrastructure Reliability Analysis of Railway Station Areas,” in FMICS, 2019.
2018
- Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, and Ufuk Topcu, “Synthesis in pMDPs: A Tale of 1001 Parameters,” in ATVA, 2018.
- Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu, Ruohan Zhang, and Mary M. Hayhoe, “Model Checking for Safe Navigation Among Humans,” in QEST, 2018.
- Sebastian Junges et al., “Finite-State Controllers of POMDPs using Parameter Synthesis,” in UAI, 2018.
2017
- Saba Aflaki, Matthias Volk, Borzoo Bonakdarpour, Joost-Pieter Katoen, and Arne Storjohann, “Automated Fine Tuning of Probabilistic Self-Stabilizing Algorithms,” in SRDS, 2017.
- Murat Cubuktepe et al., “Sequential Convex Programming for the Efficient Verification of Parametric MDPs,” in TACAS (2), 2017.
- Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, and Matthias Volk, “Model-Based Safety Analysis for Vehicle Guidance Systems,” in SAFECOMP, 2017.
2016
- Christian Dombrowski, Sebastian Junges, Joost-Pieter Katoen, and James Gross, “Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks,” in SRDS, 2016.
- Nils Jansen, Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Lukas Westhofen, “Bounded Model Checking for Probabilistic Programs,” in ATVA, 2016.
- Francesco Leofante, Simone Vuotto, Erika Ábrahám, Armando Tacchella, and Nils Jansen, “Combining Static and Runtime Methods to Achieve Safe Standing-Up for Humanoid Robots,” in ISoLA (1), 2016.
2015
- Tim Quatmann et al., “Counterexamples for Expected Rewards,” in FM, 2015.
If there is a publication missing in some of the lists above, feel free to contact us.