9 papers
Effective Stochastic Automata Model Checking by Interval Abstraction (extended version)
Pedro R. D'Argenio, Arnd Hartmanns, Annabell Petri
Stochastic automata (SA) are a formal stochastic continuous-time model based on countdown timers whose expiration times follow general probability distributions. SA are particularl…
Multi-Objective Statistical Model Checking using Lightweight Strategy Sampling (extended version)
Pedro R. D'Argenio, Arnd Hartmanns, Patrick Wienhöft +1
Statistical model checking delivers quantitative verification results with statistical guarantees. It scales to model sizes and model types that are out of reach for exhaustive, an…
UMB: A Unified Markov Binary Format for Probabilistic Model Checking (extended version)
Roman Andriushchenko, Arnd Hartmanns, Joshua Jeppson +5
This paper presents the unified Markov binary (UMB) format, an efficient, extensible, and well-supported explicit-state file format for representing a wide range of probabilistic s…
Probabilistic Verification for Modular Network-on-Chip Systems (extended version)
Nick Waddoups, Jonah Boe, Arnd Hartmanns +4
Quantitative verification can provide deep insights into reliable Network-On-Chip (NoC) designs. It is critical to understanding and mitigating operational issues caused by power s…
A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz +2
We present an efficiently executable, formally verified implementation of interval iteration for MDPs. Our correctness proofs span the entire development from the high-level abstra…
Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality (extended version)
Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer +2
Statistical model checking (SMC) randomly samples probabilistic models to approximate quantities of interest with statistical error guarantees. It is traditionally used to estimate…