A Modest Approach to Checking Probabilistic Timed Automata. - Arnd Hartmanns; Holger Hermanns (QEST, 2009)

Model-Checking and Simulation for Stochastic Timed Systems. - Arnd Hartmanns (FMCO, 2010)

Partial Order Methods for Statistical Model Checking and Simulation. - Jonathan Bogdoll; Luis María Ferrer Fioriti; Arnd Hartmanns; Holger Hermanns (FMOODS/FORTE, 2011)

Modeling of Networked Automation Systems for simulation and model checking of time behavior. - Birgit Vogel-Heuser; Jens Folmer; Georg Frey; Liu Liu 019; Holger Hermanns; Arnd Hartmanns (SSD, 2012)

State-of-the-art tools and techniques for quantitative modeling and analysis of embedded systems. - Marius Bozga; Alexandre David; Arnd Hartmanns; Holger Hermanns; Kim G. Larsen; Axel Legay; Jan Tretmans (DATE, 2012)

MODEST - A unified language for quantitative models. - Arnd Hartmanns (FDL, 2012)

Modelling and Decentralised Runtime Control of Self-stabilising Power Micro Grids. - Arnd Hartmanns; Holger Hermanns (ISoLA (1), 2012)

Simulation and Statistical Model Checking for Modestly Nondeterministic Models. - Jonathan Bogdoll; Arnd Hartmanns; Holger Hermanns (MMB/DFT, 2012)

mctau: Bridging the Gap between Modest and UPPAAL. - Jonathan Bogdoll; Alexandre David; Arnd Hartmanns; Holger Hermanns (SPIN, 2012)

A comparative analysis of decentralized power grid stabilization strategies. - Arnd Hartmanns; Holger Hermanns; Pascal Berrang (WSC, 2012)

On-the-Fly Confluence Detection for Statistical Model Checking. - Arnd Hartmanns; Mark Timmer (NASA Formal Methods, 2013)

A compositional modelling and analysis framework for stochastic hybrid systems. - Ernst Moritz Hahn; Arnd Hartmanns; Holger Hermanns; Joost-Pieter Katoen (Formal Methods Syst. Des., 2013)

An Internet Inspired Approach to Power Grid Stability. - Holger Hermanns; Arnd Hartmanns (it Inf. Technol., 2013)

The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification. - Arnd Hartmanns; Holger Hermanns (TACAS, 2014)

Reachability and Reward Checking for Stochastic Timed Automata. - Ernst Moritz Hahn; Arnd Hartmanns; Holger Hermanns (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2014)

Explicit Model Checking of Very Large MDP Using Partitioning and Secondary Storage. - Arnd Hartmanns; Holger Hermanns (ATVA, 2015)

Computing Response Time Distributions Using Iterative Probabilistic Model Checking. - Freek van den Berg; Jozef Hooman; Arnd Hartmanns; Boudewijn R. Haverkort; Anne Remke (EPEW, 2015)

In the quantitative automata zoo. - Arnd Hartmanns; Holger Hermanns (Sci. Comput. Program., 2015)

Sound statistical model checking for MDP using partial order and confluence reduction. - Arnd Hartmanns; Mark Timmer (Int. J. Softw. Tools Technol. Transf., 2015)

On the analysis of stochastic timed systems. - Arnd Hartmanns (2015)

Schedulers are no Prophets. - Arnd Hartmanns; Holger Hermanns; Jan Krcál (Semantics, Logics, and Calculi, 2016)

Flexible support for time and costs in scenario-aware dataflow. - Arnd Hartmanns; Holger Hermanns; Michael Bungert (EMSOFT, 2016)

Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata. - Pedro R. D'Argenio; Arnd Hartmanns; Axel Legay; Sean Sedwards (IFM, 2016)

A Comparison of Time- and Reward-Bounded Probabilistic Model Checking Techniques. - Ernst Moritz Hahn; Arnd Hartmanns (SETTA, 2016)

Efficient Algorithms for Time- and Cost-Bounded Probabilistic Model Checking. - Ernst Moritz Hahn; Arnd Hartmanns (CoRR, 2016)

Modelling and certification for electric mobility. - Alexander Graf-Brill; Arnd Hartmanns; Holger Hermanns; Steffen Rose (INDIN, 2017)

Better Automated Importance Splitting for Transient Rare Events. - Carlos E. Budde; Pedro R. D'Argenio; Arnd Hartmanns (SETTA, 2017)

JANI: Quantitative Model and Tool Interaction. - Carlos E. Budde; Christian Dehnert; Ernst Moritz Hahn; Arnd Hartmanns; Sebastian Junges; Andrea Turrini (TACAS (2), 2017)

Efficient simulation-based verification of probabilistic timed automata. - Arnd Hartmanns; Sean Sedwards; Pedro R. D'Argenio (WSC, 2017)

ARCH-COMP18 Category Report: Stochastic Modelling. - Alessandro Abate; Henk A. P. Blom; Nathalie Cauchi; Sofie Haesaert; Arnd Hartmanns; Kendra Lesser; Meeko Oishi; Vignesh Sivaramakrishnan; Sadegh Soudjani; Cristian Ioan Vasile; Abraham P. Vinod (ARCH@ADHS, 2018)

A Hierarchy of Scheduler Classes for Stochastic Automata. - Pedro R. D'Argenio; Marcus Gerhold; Arnd Hartmanns; Sean Sedwards (FoSSaCS, 2018)

Lightweight Statistical Model Checking in Nondeterministic Continuous Time. - Pedro R. D'Argenio; Arnd Hartmanns; Sean Sedwards (ISoLA (2), 2018)

Model-Based Testing for General Stochastic Time. - Marcus Gerhold; Arnd Hartmanns; Mariëlle Stoelinga (NFM, 2018)

A Statistical Model Checker for Nondeterminism and Rare Events. - Carlos E. Budde; Pedro R. D'Argenio; Arnd Hartmanns; Sean Sedwards (TACAS (2), 2018)

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

Probabilistic Verification for Reliable Network-on-Chip System Design. - Benjamin Lewis; Arnd Hartmanns; Prabal Basu; Rajesh Jayashankara Shridevi; Koushik Chakraborty; Sanghamitra Roy; Zhen Zhang 006 (FMICS, 2019)

A Modest Approach to Modelling and Checking Markov Automata. - Yuliya Butkova; Arnd Hartmanns; Holger Hermanns (QEST, 2019)

A Modest Markov Automata Tutorial. - Arnd Hartmanns; Holger Hermanns (RW, 2019)

TOOLympics 2019: An Overview of Competitions in Formal Methods. - Ezio Bartocci; Dirk Beyer 001; Paul E. Black; Grigory Fedyukovich; Hubert Garavel; Arnd Hartmanns; Marieke Huisman; Fabrice Kordon; Julian Nagele; Mihaela Sighireanu; Bernhard Steffen; Martin Suda 001; et al. (TACAS (3), 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)

Model-based testing of stochastically timed systems. - Marcus Gerhold; Arnd Hartmanns; Mariëlle Stoelinga (Innov. Syst. Softw. Eng., 2019)

Automated compositional importance splitting. - Carlos E. Budde; Pedro R. D'Argenio; Arnd Hartmanns (Sci. Comput. Program., 2019)

ARCH-COMP20 Category Report: Stochastic Models. - Alessandro Abate; Henk A. P. Blom; Nathalie Cauchi; Joanna Delicaris; Arnd Hartmanns; Mahmoud Khaled; Abolfazl Lavaei; Carina Pilch; Anne Remke; Stefan Schupp; Fedor Shmarov; Sadegh Soudjani; et al. (ARCH, 2020)

Optimistic Value Iteration. - Arnd Hartmanns; Benjamin Lucien Kaminski (CAV (2), 2020)

Classic and non-prophetic model checking for hybrid Petri nets with stochastic firings. - Carina Pilch; Arnd Hartmanns; Anne Remke (HSCC, 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)

Sampling Distributed Schedulers for Resilient Space Communication. - Pedro R. D'Argenio; Juan A. Fraire; Arnd Hartmanns (NFM, 2020)

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

An efficient statistical model checker for nondeterminism and rare events. - Carlos E. Budde; Pedro R. D'Argenio; Arnd Hartmanns; Sean Sedwards (Int. J. Softw. Tools Technol. Transf., 2020)

ARCH-COMP21 Category Report: Stochastic Models. - Alessandro Abate; Henk A. P. Blom; Marc Bouissou; Nathalie Cauchi; Hassane Chraibi; Joanna Delicaris; Sofie Haesaert; Arnd Hartmanns; Mahmoud Khaled; Abolfazl Lavaei; Hao Ma; Kaushik Mallik; et al. (ARCH@ADHS, 2021)

Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System. - Riley Roberts; Benjamin Lewis; Arnd Hartmanns; Prabal Basu; Sanghamitra Roy; Koushik Chakraborty; Zhen Zhang 006 (FMICS, 2021)

Learning optimal decisions for stochastic hybrid systems. - Mathis Niehage; Arnd Hartmanns; Anne Remke (MEMOCODE, 2021)

Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids. - Thom S. Badings; Arnd Hartmanns; Nils Jansen 001; Marnix Suilen (NFM, 2021)

Tweaking the Odds in Probabilistic Timed Automata. - Arnd Hartmanns; Joost-Pieter Katoen; Bram Kohlen; Jip Spel (QEST, 2021)

Symblicit exploration and elimination for probabilistic model checking. - Ernst Moritz Hahn; Arnd Hartmanns (SAC, 2021)

Replicating sc Restart with Prolonged Retrials: An Experimental Report. - Carlos E. Budde; Arnd Hartmanns (TACAS (2), 2021)

A Modest Approach to Markov Automata. - Yuliya Butkova; Arnd Hartmanns; Holger Hermanns (ACM Trans. Model. Comput. Simul., 2021)

ARCH-COMP22 Category Report: Stochastic Models. - Alessandro Abate; Henk A. P. Blom; Joanna Delicaris; Sofie Haesaert; Arnd Hartmanns; Birgit van Huijgevoort; Abolfazl Lavaei; Hao Ma; Mathis Niehage; Anne Remke; Oliver Schön; Stefan Schupp; et al. (ARCH@SAFECOMP, 2022)

The Modest State of Learning, Sampling, and Verifying Strategies. - Arnd Hartmanns; Michaela Klauck (ISoLA (3), 2022)

Comparing Statistical and Analytical Routing Approaches for Delay-Tolerant Networks. - Pedro R. D'Argenio; Juan A. Fraire; Arnd Hartmanns; Fernando D. Raverta (QEST, 2022)

Correct Probabilistic Model Checking with Floating-Point Arithmetic. - Arnd Hartmanns (TACAS (2), 2022)

An Overview of Modest Models and Tools for Real Stochastic Timed Systems. - Arnd Hartmanns (MARS@ETAPS, 2022)

Backwards Reachability for Probabilistic Timed Automata: A Replication Report. - Arnd Hartmanns; Bram Kohlen (CoRR, 2022)

Fast Verified SCCs for Probabilistic Model Checking. - Arnd Hartmanns; Bram Kohlen; Peter Lammich (ATVA (1), 2023)

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)

Reproduction Report for SV-COMP 2023. - Marcus Gerhold; Arnd Hartmanns (CoRR, 2023)

Modest Models and Tools for Real Stochastic Timed Systems. - Carlos E. Budde; Pedro R. D'Argenio; Juan A. Fraire; Arnd Hartmanns; Zhen Zhang 006 (Principles of Verification (2), 2024)

Efficient Formally Verified Maximal End Component Decomposition for MDPs. - Arnd Hartmanns; Bram Kohlen; Peter Lammich (FM (1), 2024)

Digging for Decision Trees: A Case Study in Strategy Sampling and Learning. - Carlos E. Budde; Pedro R. D'Argenio; Arnd Hartmanns (AISoLA, 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)

A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs. - Bram Kohlen; Maximilian Schäffeler; Mohammad Abdulaziz; Arnd Hartmanns; Peter Lammich (CAV (2), 2025)

An Overview of Sound and Modest Approaches to Quantitative Model Checking from Sea to Space. - Arnd Hartmanns (FMICS, 2025)

Rare Event Simulation for Stochastic Hybrid Systems Using Symbolic Importance Functions. - Mathis Niehage; Carina da Silva; Anne Remke; Arnd Hartmanns (NFM, 2025)

Sound Statistical Model Checking for Probabilities and Expected Rewards. - Carlos E. Budde; Arnd Hartmanns; Tobias Meggendorfer; Maximilian Weininger; Patrick Wienhöft (TACAS (1), 2025)

Comparing Statistical, Analytical, and Learning-Based Routing Approaches for Delay-Tolerant Networks. - Pedro R. D'Argenio; Juan A. Fraire; Arnd Hartmanns; Fernando D. Raverta (ACM Trans. Model. Comput. Simul., 2025)

Time-Sensitive Importance Splitting. - Gabriel Dengler; Carlos E. Budde; Laura Carnevali; Arnd Hartmanns (CoRR, 2025)