Arnd Hartmanns
I am an associate professor in the Formal Methods and Tools group at the University of Twente.
My primary research interests are modelling tools and formalisms for stochastic timed and hybrid systems (in particular Modest) and their applications in various fields.
I advocate reproducibility in Computer Science research, via artifact evaluation initiatives, tool competitions, and standardised benchmark sets.
I was previously a postdoc in the Formal Methods and Tools group at the University of Twente and the Dependable Systems and Software group at Saarland University, where I also completed my Ph.D. in computer science with a thesis On the Analysis of Stochastic Timed Systems in 2015.
Contact
| University of Twente |
| Room: |
Zilverling 3061 |
| E-Mail: |
|
Projects
Committees
I was previously a member of the program committees for
ICSOB 2024,
MARS 2024, and
QEST-FORMATS 2024
2024; for
FormaliSE,
QEST, and
SPIN,
2023; for
FORMATS and
FORTE
2022; for
FORMATS,
SNR, and
SPIN
2021; for
FORMATS,
QEST, and
SBMF
2020; for
QEST and
SETTA
2019; for
FORTE
2018; and for
ACSD
2017.
Publications
[DBLP] [Google Scholar]
2025
-
PyDSMC: Statistical Model Checking for Neural Agents Using the Gymnasium Interface
with Timo P. Gros, Ivo Hoese, Joshua Meyer, Nicola J. Müller, and Verena Wolf:
QEST+FORMATS 2025, Aarhus, Denmark (August 2025, to appear)
-
Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality
with Carlos E. Budde, Tobias Meggendorfer, Maximilian Weininger, and Patrick Wienhöft:
QEST+FORMATS 2025, Aarhus, Denmark (August 2025, to appear)
-
Time-Sensitive Importance Splitting
with Gabriel Dengler, Carlos E. Budde, and Laura Carnevali:
QEST+FORMATS 2025, Aarhus, Denmark (August 2025, to appear)
-
A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
with Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz, and Peter Lammich:
CAV 2025, Zagreb, Croatia (July 2025, to appear)
[arXiv]
-
Rare Event Simulation for Stochastic Hybrid Systems using Symbolic Importance Functions
with Mathis Niehage, Carina da Silva, and Anne Remke:
NASA Formal Methods 2025, Williamsburg, VA, USA (June 2025, to appear)
-
Sound Statistical Model Checking for Probabilities and Expected Rewards
with Carlos E. Budde, Tobias Meggendorfer, Maximilian Weininger, and Patrick Wienhöft:
TACAS 2025, Hamilton, Canada (May 2025)
[DOI]
-
Comparing Statistical, Analytical, and Learning-Based Routing Approaches for Delay-Tolerant Networks
with Pedro R. D'Argenio, Juan A. Fraire, and Fernando Raverta:
ACM Transactions on Modeling and Computer Simulation (April 2025)
[DOI]
2024
-
Modest Models and Tools for Real Stochastic Timed Systems
with Carlos E. Budde, Pedro R. D'Argenio, Juan A. Fraire, and Zhen Zhang:
Principles of Verification, Aachen, Germany (November 2024)
[DOI]
-
Digging for Decision Trees: A Case Study in Strategy Sampling and Learning
with Carlos E. Budde and Pedro R. D'Argenio:
AISoLA 2024, Crete, Greece (November 2024)
[DOI]
-
Efficient Formally Verified Maximal End Component Decomposition for MDPs
with Bram Kohlen and Peter Lammich:
FM 2024, Milan, Italy (September 2024)
[DOI]
2023
-
Fast Verified SCCs for Probabilistic Model Checking
with Bram Kohlen and Peter Lammich:
ATVA 2023, Singapore (October 2023)
[DOI]
-
A Practitioner's Guide to MDP Model Checking
with Sebastian Junges, Tim Quatmann, and Maximilian Weininger:
TACAS 2023, Paris, France (April 2023)
[DOI]
-
Tools at the Frontiers of Quantitative Verification (QComp 2023 Competition Report)
with Roman Andriushchenko, Alexander Bork, Carlos E. Budde, Milan Češka, Ernst Moritz Hahn, Bryant Israelsen, Nils Jansen, Joshua Jeppson, Sebastian Junges, Maximilian A. Köhl, Bettina Könighofer, Jan Křetínský, Tobias Meggendorfer, David Parker, Stefan Pranger, Tim Quatmann, Enno Ruijters, Landon Taylor, Matthias Volk, Maximilian Weininger, and Zhen Zhang:
TOOLympics 2023, Paris, France (April 2023)
[DOI]
2022
-
The Modest State of Learning, Sampling, and Verifying Strategies
with Michaela Klauck,
ISoLA 2022, Rhodes, Greece (October 2022)
[DOI]
-
Comparing Statistical and Analytical Routing Approaches for Delay-Tolerant Networks
with Pedro R. D'Argenio, Juan A. Fraire, and Fernando Raverta:
QEST 2022, Warsaw, Poland (September 2022)
[DOI]
-
Correct Probabilistic Model Checking with Floating-Point Arithmetic
TACAS 2022, Munich, Germany (April 2022)
[DOI]
-
An Overview of Modest Models and Tools for Real Stochastic Timed Systems
MARS 2022, Munich, Germany (April 2022)
[DOI]
2021
-
Learning Optimal Decisions for Stochastic Hybrid Systems
with Mathis Niehage and Anne Remke:
MEMOCODE 2021, Beijing, China (November 2021)
[DOI]
-
Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System
with Riley Roberts, Benjamin Lewis, Prabal Basu, Sanghamitra Roy, Koushik Chakraborty, and Zhen Zhang:
FMICS 2021, Paris, France (August 2021)
[DOI]
-
Tweaking the Odds in Probabilistic Timed Automata
with Joost-Pieter Katoen, Bram Kohlen, and Jip Spel:
QEST 2021, Paris, France (August 2021)
[DOI]
-
A Modest Approach to Markov Automata
with Yuliya Butkova and Holger Hermanns:
ACM Transactions on Modeling and Computer Simulation (July 2021)
[DOI]
-
Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids
with Thom S. Badings, Nils Jansen, and Marnix Suilen:
NASA Formal Methods 2021, Norfolk, VA, USA (May 2021)
[DOI]
-
Replicating Restart with Prolonged Retrials: An Experimental Report
with Carlos E. Budde:
TACAS 2021, Luxembourg, Luxembourg (March 2021)
[DOI]
-
Symblicit Exploration and Elimination for Probabilistic Model Checking
with Ernst Moritz Hahn:
ACM SAC 2021, Gwangju, South Korea (March 2021)
[DOI]
2020
-
An Efficient Statistical Model Checker for Nondeterminism and Rare Events
with Carlos E. Budde, Pedro R. D'Argenio and Sean Sedwards:
Software Tools for Technology Transfer (November 2020)
[DOI]
-
On Correctness, Precision, and Performance in Quantitative Verification (QComp 2020 Competition Report)
with Carlos E. Budde, Michaela Klauck, Jan Křetínský, David Parker, Tim Quatmann, Andrea Turrini, and Zhen Zhang:
ISoLA 2020, Rhodes, Greece (October 2020)
[DOI]
-
Multi-cost Bounded Tradeoff Analysis in MDP
with Sebastian Junges, Joost-Pieter Katoen, and Tim Quatmann:
Journal of Automated Reasoning (October 2020)
[DOI]
-
Optimistic Value Iteration
with Benjamin Lucien Kaminski:
CAV 2020, Los Angeles, CA, USA (July 2020)
[DOI]
-
Sampling Distributed Schedulers for Resilient Space Communication
with Pedro R. D'Argenio and Juan A. Fraire:
NASA Formal Methods 2020, Moffet Field, CA, USA (May 2020)
[DOI]
-
Classic and Non-Prophetic Model Checking for Hybrid Petri Nets with Stochastic Firings
with Carina Pilch and Anne Remke:
HSCC 2020, Sydney, Australia (April 2020)
[DOI]
2019
-
A Modest Markov Automata Tutorial
with Holger Hermanns:
RW 2019, Bolzano, Italy (September 2019)
[DOI]
-
A Modest Approach to Modelling and Checking Markov Automata
with Yuliya Butkova and Holger Hermanns:
QEST 2019, Glasgow, United Kingdom (September 2019)
[DOI]
-
Model-Based Testing of Stochastically Timed Systems
with Marcus Gerhold and Mariëlle Stoelinga:
Innovations in Systems and Software Engineering (September 2019)
[DOI]
-
Probabilistic Verification for Reliable Network-on-Chip System Design
with Prabal Basu, Koushik Chakraborty, Rajesh Jayashankara Shridevi, Benjamin Lewis, Sanghamitra Roy, and Zhen Zhang:
FMICS 2019, Amsterdam, The Netherlands (August 2019)
[DOI]
-
Automated Compositional Importance Splitting
with Carlos E. Budde and Pedro R. D'Argenio:
Science of Computer Programming (April 2019)
[PDF] [DOI]
-
The Quantitative Verification Benchmark Set
with Michaela Klauck, David Parker, Tim Quatmann, and Enno Ruijters:
TACAS 2019, Prague, Czech Republic (April 2019)
[DOI]
-
The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models
with Ernst Moritz Hahn, Christian Hensel, Michaela Klauck, Joachim Klein, Jan Kretínský, David Parker, Tim Quatmann, Enno Ruijters, and Marcel Steinmetz:
TACAS 2019, Prague, Czech Republic (April 2019)
[DOI]
2018
-
Lightweight Statistical Model Checking in Nondeterministic Continuous Time
with Pedro R. D'Argenio and Sean Sedwards:
ISoLA 2018, Limassol, Cyprus (November 2018)
[DOI]
-
A Statistical Model Checker for Nondeterminism and Rare Events
with Carlos E. Budde, Pedro R. D'Argenio, and Sean Sedwards:
TACAS 2018, Thessaloniki, Greece (April 2018)
[DOI]
-
Multi-Cost Bounded Reachability in MDP
with Sebastian Junges, Joost-Pieter Katoen, and Tim Quatmann:
TACAS 2018, Thessaloniki, Greece (April 2018)
[DOI]
-
A Hierarchy of Scheduler Classes for Stochastic Automata
with Pedro R. D'Argenio, Marcus Gerhold, and Sean Sedwards:
FoSSaCS 2018, Thessaloniki, Greece (April 2018)
[DOI]
-
Model-Based Testing for General Stochastic Time
with Marcus Gerhold and Mariëlle Stoelinga:
NASA Formal Methods 2018, Newport News, VA, USA (April 2018)
[DOI]
2017
-
Efficient Simulation-Based Verification of Probabilistic Timed Automata
with Pedro R. D'Argenio and Sean Sedwards:
WinterSim 2017, Las Vegas, NV, USA (December 2017)
[DOI]
-
Better Automated Importance Splitting for Transient Rare Events
with Carlos E. Budde and Pedro R. D'Argenio:
SETTA 2017, Changsha, China (October 2017)
[DOI]
-
Modelling and Certification for Electric Mobility
with Alexander Graf-Brill and Holger Hermanns:
INDIN 2017, Emden, Germany (July 2017)
[DOI]
-
JANI: Quantitative Model and Tool Interaction
with Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn, Sebastian Junges, and Andrea Turrini:
TACAS 2017, Uppsala, Sweden (April 2017)
[DOI]
2016
-
A Comparison of Time- and Reward-Bounded Probabilistic Model Checking Techniques
with Ernst Moritz Hahn:
SETTA 2016, Beijing, China (November 2016)
[DOI]
-
Flexible Support for Time and Costs in Scenario-Aware Dataflow
with Michael Bungert and Holger Hermanns:
EMSOFT 2016, Pittsburgh, PA, USA (October 2016)
[PDF]
-
Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata
with Sean Sedwards, Pedro R. D'Argenio, and Axel Legay:
iFM 2016, Reykjavík, Iceland (June 2016)
[DOI]
-
Schedulers are no Prophets
with Holger Hermanns and Jan Krčál:
Nielson² Colloquium, Kongens Lyngby, Denmark (January 2016)
[DOI]
2015
-
In the Quantitative Automata Zoo
with Holger Hermanns:
Science of Computer Programming (November 2015)
[DOI]
-
Explicit Model Checking of Very Large MDP using Partitioning and Secondary Storage
with Holger Hermanns:
ATVA 2015, Shanghai, China (October 2015)
[DOI]
-
Computing Response Time Distributions using Iterative Probabilistic Model Checking
with Freek van den Berg, Jozef Hooman, Boudewijn Haverkort, and Anne Remke:
EPEW 2015, Madrid, Spain (August-September 2015)
[DOI]
-
Sound Statistical Model Checking for MDP using Partial Order and Confluence Reduction
with Mark Timmer:
Software Tools for Technology Transfer (August 2015)
[DOI] [PDF]
2014
-
Reachability and Reward Checking for Stochastic Timed Automata
with Ernst Moritz Hahn and Holger Hermanns:
AVoCS 2014, Enschede, The Netherlands (September 2014)
[PDF]
-
The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification
with Holger Hermanns:
TACAS 2014, Grenoble, France (April 2014)
[DOI]
2013
-
A Compositional Modelling and Analysis Framework for Stochastic Hybrid Systems
with Ernst Moritz Hahn, Holger Hermanns, and Joost-Pieter Katoen:
Formal Methods in System Design (October 2013)
[DOI] [PDF]
-
On-the-fly Confluence Detection for Statistical Model Checking
with Mark Timmer:
NASA Formal Methods 2013, Moffett Field, CA, USA (May 2013)
[DOI]
-
An Internet Inspired Approach to Power Grid Stability
with Holger Hermanns:
it – Information Technology (April 2013)
[DOI]
2012
-
A Comparative Analysis of Decentralized Power Grid Stabilization Strategies
with Pascal Berrang and Holger Hermanns:
WinterSim 2012, Berlin, Germany (December 2012)
[DOI] [PDF]
-
Modelling and Decentralised Runtime Control of Self-stabilising Power Micro Grids
with Holger Hermanns:
ISoLA 2012, Heraclion, Greece (October 2012)
[DOI]
-
Modest – A Unified Language for Quantitative Models
FDL 2012, Vienna, Austria (September 2012)
[IEEE]
-
mctau: Bridging the Gap between Modest and UPPAAL
with Jonathan Bogdoll, Alexandre David, and Holger Hermanns:
SPIN 2012, Oxford, United Kingdom (July 2012)
[DOI]
-
Modeling of Networked Automation Systems for Simulation and Model Checking of Time Behavior
with Jens Folmer, Georg Frey, Holger Hermanns, Liu Liu, and Birgit Vogel-Heuser:
SSD/SAC 2012, Chemnitz, Germany (March 2012)
[DOI]
-
Simulation and Statistical Model Checking for Modestly Nondeterministic Models
with Jonathan Bogdoll and Holger Hermanns:
MMB/DFT 2012, Kaiserslautern, Germany (March 2012)
[DOI]
-
State-of-the-art Tools and Techniques for Quantitative Modeling and Analysis of Embedded Systems
with Marius Bozga, Alexandre David, Holger Hermanns, Kim G. Larsen, Axel Legay, and Jan Tretmans:
DATE 2012, Dresden, Germany (March 2012)
[IEEE]
2011
-
Partial Order Methods for Statistical Model Checking and Simulation
with Jonathan Bogdoll, Luis María Ferrer Fioriti, and Holger Hermanns:
FMOODS/FORTE 2011, Reykjavík, Iceland (June 2011)
[DOI]
2010
-
Model-Checking and Simulation for Stochastic Timed Systems
FMCO 2010, Graz, Austria (December 2010)
[DOI]
2009
-
A Modest Approach to Checking Probabilistic Timed Automata
with Holger Hermanns:
QEST 2009, Budapest, Hungary (September 2009)
[DOI]
Teaching
University of Twente
-
Spring 2024, 2025:
Quantitative Evaluation of Systems (lecturer, examiner)
Core elective course (5 EC)
in the Software Technology specialisation of the Computer Science M.Sc. programme
and elective course in the Embedded Systems M.Sc. programme.
-
Spring 2021, 2023, 2025:
Probabilistic Model Checking (lecturer, examiner, with Ernst Moritz Hahn)
Advanced elective course (5 EC)
in the Software Technology specialisation of the Computer Science M.Sc. programme.
-
Summer 2021, ..., 2025:
Programming Paradigms (coordinator)
Elective module (15 EC) comprising 5 separate but integrated courses in the Technical Computer Science B.Sc. programme.
-
Summer 2019, ..., 2023:
Compiler Construction (lecturer, examiner)
Course within the Technical Computer Science B.Sc. module Programming Paradigms.
-
Winter 2018, ..., 2022:
Quantitative Evaluation of Embedded Systems (lecturer, examiner)
Core course (5 EC)
in the Embedded Systems M.Sc. programme.
-
Spring 2016, ..., 2020:
Software Testing and Reverse Engineering (local coordinator)
Advanced elective course (5 EC) by Sicco Verwer
at Delft University of Technology
in the joint Cyber Security M.Sc. programme with the University of Twente.
-
Spring 2018:
Programming in Python (lecturer)
Preparation course
on programming in Python and graph algorithms,
part of the joint Applied Mathematics and Technical Computer Science B.Sc. module Discrete Structures and Efficient Algorithms.
-
Spring 2016, 2017 and 2018:
Languages and Machines (assistant)
Base course by Jaco van de Pol
on foundations of theoretical computer science,
part of the joint Applied Mathematics and Technical Computer Science B.Sc. module Discrete Structures and Efficient Algorithms.
-
Winter 2017:
Dependable Systems and Networks (assistant)
Course by Boudewijn Haverkort
on the design and evaluation of dependable systems,
part of the joint Electrical Engineering and Technical Computer Science B.Sc. elective module Cyber-Physical Systems.
Saarland University
Theses
-
On the Analysis of Stochastic Timed Systems, Ph.D. Thesis, Universität des Saarlandes, February 2015
[PDF]
(received the 2016 Best Dissertation Award by the GI/ITG Technical Committee for "Measurement, Modelling and Evaluation of Computing Systems")
-
A Modest Checker for Probabilistic Timed Automata, Master's Thesis, Universität des Saarlandes, March 2009
-
Value Passing in Modest, Bachelor's Thesis, Universität des Saarlandes, May 2007
[PDF]
Reviewing
Conferences:
FORMATS, ICSE, and SPIN 2021;
FORMATS, NFM, QEST, TACAS, and TTCS 2020;
COCOON, QEST, SETTA, and TACAS 2019;
FMCAD, FORTE, ISoLA, and TACAS 2018;
ACSD, TACAS, and WSC 2017;
ACSD, ICFEM, and MFCS 2016;
ATVA and TACAS 2015;
HSCC and QEST 2014;
ESOP, HSCC, and VMCAI 2013;
AVoCS, FMICS, HSCC, and TACAS 2012;
ATVA, CAV, FORMATS, FMICS, and HSCC 2011;
CAV, DSN, FORMATS, FMCO, and MMB/DFT 2010;
AVoCS and CONCUR 2009.
Journals:
ACM Transactions on Modeling and Computer Simulation (2018),
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (2013),
Information and Computation (2017, 2018),
IT Professional (2021),
Journal of Logical and Algebraic Methods in Programming (2017, 2018),
Logical Methods in Computer Science (2020),
Software Tools for Technology Transfer (2014, 2015, 2017),
and
Theoretical Computer Science (2013, 2016, 2017, 2020).
Other
Founding director of The Weissbord Institute.