Counterexamples for Expected Rewards. - Tim Quatmann; Nils Jansen 001; Christian Dehnert; Ralf Wimmer 001; Erika Ábrahám; Joost-Pieter Katoen; Bernd Becker 001 (FM, 2015)

Parameter Synthesis for Markov Models: Faster Than Ever. - Tim Quatmann; Christian Dehnert; Nils Jansen 001; Sebastian Junges; Joost-Pieter Katoen (ATVA, 2016)

Permissive Finite-State Controllers of POMDPs using Parameter Synthesis. - Sebastian Junges; Nils Jansen 001; Ralf Wimmer 001; Tim Quatmann; Leonore Winterer; Joost-Pieter Katoen; Bernd Becker 001 (CoRR, 2017)

Sound Value Iteration. - Tim Quatmann; Joost-Pieter Katoen (CAV (1), 2018)

Multi-cost Bounded Reachability in MDP. - Arnd Hartmanns; Sebastian Junges; Joost-Pieter Katoen; Tim Quatmann (TACAS (2), 2018)

Finite-State Controllers of POMDPs using Parameter Synthesis. - Sebastian Junges; Nils Jansen 001; Ralf Wimmer 001; Tim Quatmann; Leonore Winterer; Joost-Pieter Katoen; Bernd Becker 001 (UAI, 2018)

Correct-by-construction policies for POMDPs. - Nils Jansen 001; Sebastian Junges; Joost-Pieter Katoen; Tim Quatmann; Bernd Becker 001; Ralf Wimmer 001; Leonore Winterer (SNR, 2019)

The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report). - Ernst Moritz Hahn; Arnd Hartmanns; Christian Hensel; Michaela Klauck; Joachim Klein 001; Jan Kretínský; David Parker 001; Tim Quatmann; Enno Ruijters; Marcel Steinmetz (TACAS (3), 2019)

The Quantitative Verification Benchmark Set. - Arnd Hartmanns; Michaela Klauck; David Parker 001; Tim Quatmann; Enno Ruijters (TACAS (1), 2019)

Parameter Synthesis for Markov Models. - Sebastian Junges; Erika Ábrahám; Christian Hensel; Nils Jansen 001; Joost-Pieter Katoen; Tim Quatmann; Matthias Volk 001 (CoRR, 2019)

Simple Strategies in Multi-Objective MDPs (Technical Report). - Florent Delgrange; Joost-Pieter Katoen; Tim Quatmann; Mickael Randour (CoRR, 2019)

Verification of Indefinite-Horizon POMDPs. - Alexander Bork; Sebastian Junges; Joost-Pieter Katoen; Tim Quatmann (ATVA, 2020)

On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report. - Carlos E. Budde; Arnd Hartmanns; Michaela Klauck; Jan Kretínský; David Parker 001; Tim Quatmann; Andrea Turrini; Zhen Zhang 006 (ISoLA (4), 2020)

Simple Strategies in Multi-Objective MDPs. - Florent Delgrange; Joost-Pieter Katoen; Tim Quatmann; Mickael Randour (TACAS (1), 2020)

Multi-cost Bounded Tradeoff Analysis in MDP. - Arnd Hartmanns; Sebastian Junges; Joost-Pieter Katoen; Tim Quatmann (J. Autom. Reason., 2020)

Multi-objective Optimization of Long-run Average and Total Rewards: Supplemental Material. - Tim Quatmann; Joost-Pieter Katoen (Zenodo, 2020)

Multi-objective Optimization of Long-run Average and Total Rewards: Supplemental Material. - Tim Quatmann; Joost-Pieter Katoen (Zenodo, 2020)

Multi-objective Optimization of Long-run Average and Total Rewards. - Tim Quatmann; Joost-Pieter Katoen (TACAS (1), 2021)

Artifact for Paper: Under-Approximating Expected Total Rewards in POMDPs. - Alexander Bork; Joost-Pieter Katoen; Tim Quatmann (Zenodo, 2021)

Update Package for Artifact for Paper: Under-Approximating Expected Total Rewards in POMDPs. - Alexander Bork; Joost-Pieter Katoen; Tim Quatmann (Zenodo, 2021)

Artifact for Paper: Under-Approximating Expected Total Rewards in POMDPs. - Alexander Bork; Joost-Pieter Katoen; Tim Quatmann (Zenodo, 2021)

Artifact for Paper: Under-Approximating Expected Total Rewards in POMDPs. - Alexander Bork; Joost-Pieter Katoen; Tim Quatmann (Zenodo, 2021)

Under-Approximating Expected Total Rewards in POMDPs. - Alexander Bork; Joost-Pieter Katoen; Tim Quatmann (TACAS (2), 2022)

The probabilistic model checker Storm. - Christian Hensel; Sebastian Junges; Joost-Pieter Katoen; Tim Quatmann; Matthias Volk 001 (Int. J. Softw. Tools Technol. Transf., 2022)

Markov automata with multiple objectives. - Tim Quatmann; Sebastian Junges; Joost-Pieter Katoen (Formal Methods Syst. Des., 2022)

A Practitioner's Guide to MDP Model Checking Algorithms. - Arnd Hartmanns; Sebastian Junges; Tim Quatmann; Maximilian Weininger (TACAS (1), 2023)

Tools at the Frontiers of Quantitative Verification - QComp 2023 Competition Report. - Roman Andriushchenko; Alexander Bork; Carlos E. Budde; Milan Ceska 002; Kush Grover; Ernst Moritz Hahn; Arnd Hartmanns; Bryant Israelsen; Nils Jansen 001; Joshua Jeppson; Sebastian Junges; Maximilian A. Köhl; et al. (TOOLympics@ETAPS, 2023)

Verification of multi-objective Markov models. - Tim Quatmann (2023)

Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains (Artifact). - Hannah Mertens; Joost-Pieter Katoen; Tim Quatmann; Tobias Winkler 001 (Zenodo, 2023)

Riding the Storm in a Probabilistic Model Checking Landscape. - Christian Hensel; Sebastian Junges; Tim Quatmann; Matthias Volk 001 (Principles of Verification (2), 2024)

A Spectrum of Approximate Probabilistic Bisimulations. - Timm Spork; Christel Baier; Joost-Pieter Katoen; Jakob Piribauer; Tim Quatmann (CONCUR, 2024)

Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains. - Hannah Mertens; Joost-Pieter Katoen; Tim Quatmann; Tobias Winkler 001 (TACAS (2), 2024)

Tools at the Frontiers of Quantitative Verification. - Roman Andriushchenko; Alexander Bork; Carlos E. Budde; Milan Ceska 002; Kush Grover; Ernst Moritz Hahn; Arnd Hartmanns; Bryant Israelsen; Nils Jansen 001; Joshua Jeppson; Sebastian Junges; Maximilian A. Köhl; et al. (CoRR, 2024)

Parameter synthesis for Markov models: covering the parameter space. - Sebastian Junges; Erika Ábrahám; Christian Hensel; Nils Jansen 001; Joost-Pieter Katoen; Tim Quatmann; Matthias Volk 001 (Formal Methods Syst. Des., 2024)

Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate (Artifact). - Hannah Mertens; Tim Quatmann; Joost-Pieter Katoen; Tobias Winkler 001 (Zenodo, 2024)

Compositional Reasoning for Parametric Probabilistic Automata. - Hannah Mertens; Tim Quatmann; Joost-Pieter Katoen (CONCUR, 2025)

Fixed Point Certificates for Reachability and Expected Rewards in MDPs. - Krishnendu Chatterjee; Tim Quatmann; Maximilian Schäffeler; Maximilian Weininger; Tobias Winkler 001; Daniel Zilken (TACAS (2), 2025)

Multi-Cost-Bounded Reachability Analysis of POMDPs. - Alexander Bork; Joost-Pieter Katoen; Tim Quatmann; Svenja Stein (UAI, 2025)

Artifact: Fixed Point Certificates for Reachability and Expected Rewards in MDPs. - Krishnendu Chatterjee; Tim Quatmann; Maximilian Schäffeler; Maximilian Weininger; Tobias Winkler 001; Daniel Zillken (Zenodo, 2025)

Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains. - Linus Heck; Tim Quatmann; Jip Spel; Joost-Pieter Katoen; Sebastian Junges (CoRR, 2025)