Arnd Hartmanns
I am an assistant 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
Publications
[DBLP] [Google Scholar]
2021
-
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 2021, Rhodes, Greece (October 2021),
to appear.
-
Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids
with Thom S. Badings, Nils Jansen, and Marnix Suilen:
NFM 2021, Norfolk, VA, USA (May 2021),
to appear.
-
A Modest Approach to Markov Automata
with Yuliya Butkova and Holger Hermanns:
ACM Transactions on Modeling and Computer Simulation,
to appear.
-
Replicating Restart with Prolonged Retrials: An Experimental Report
with Carlos E. Budde:
TACAS 2021, Luxembourg, Luxembourg (March 2021),
to appear.
-
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]
-
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:
NFM 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
-
Winter 2018, 2019, and 2020:
Quantitative Evaluation of Embedded Systems (lecturer, examiner)
Core lecture,
part of the Embedded Systems M.Sc. programme
at the University of Twente.
-
Summer 2019 and 2020:
Compiler Construction (lecturer, examiner)
Base lecture,
part of the Technical Computer Science B.Sc. module Programming Paradigms
at the University of Twente.
-
Spring 2016, ..., 2020:
Software Testing and Reverse Engineering (local coordinator)
Advanced lecture 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
at the University of Twente.
-
Spring 2016, 2017 and 2018:
Languages and Machines (assistant)
Base lecture 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
at the University of Twente.
-
Winter 2017:
Dependable Systems and Networks (assistant)
Core lecture by Boudewijn Haverkort
on the design and evaluation of dependable systems,
part of the joint Electrical Engineering and Technical Computer Science B.Sc. module Cyber-Physical Systems
at the University of Twente.
-
Summer 2015:
Data Networks (lecturer, examiner)
Core lecture on computer networks,
part of the Computer Science B.Sc. and M.Sc. programmes at Saarland University.
-
Winter 2014/15:
Verification (assistant)
Core lecture by Holger Hermanns
on verification,
part of the Computer Science B.Sc. and M.Sc. programmes at Saarland University.
-
Summer 2012:
The Automata Zoo (assistant)
Lecture by Holger Hermanns
on automata models and model checking,
part of the MCS 2012 Summer School at the University of Oldenburg.
-
Summer 2011:
Data Networks (assistant)
Core lecture by Holger Hermanns and Verena Wolf
on computer networks
in the Computer Science B.Sc. and M.Sc. programmes at Saarland University.
-
Winter 2010/11:
Im Zoo der Automaten (assistant)
Undergraduate seminar with Holger Hermanns and Moritz Hahn
focusing on presentation skills
in the Computer Science B.Sc. programme at Saarland University.
-
Winter 2009/10:
Programmierung 1 (assistant)
Base lecture by Holger Hermanns
on computer science basics using functional programming
in the Computer Science B.Sc. programme at Saarland University.
-
Summer 2008:
Nebenläufige Programmierung (student assistant)
Base lecture by Holger Hermanns
on concurrent programming and concurrency theory
in the Computer Science B.Sc. programme at Saarland University.
-
Summer 2007:
Informationssysteme (student assistant)
Base lecture by Christoph Koch
on databases and information systems
in the Computer Science B.Sc. programme at Saarland University.
-
Winter 2005/06:
Programmierung 1 (student assistant)
Base lecture by Holger Hermanns
on computer science basics using functional programming
in the Computer Science B.Sc. programme at 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:
AVoCS and CONCUR 2009,
CAV, DSN, FORMATS, FMCO and MMB/DFT 2010,
ATVA, CAV, FORMATS, FMICS and HSCC 2011,
AVoCS, FMICS, HSCC and TACAS 2012,
ESOP, HSCC and VMCAI 2013,
HSCC and QEST 2014,
ATVA and TACAS 2015,
ACSD, ICFEM and MFCS 2016,
ACSD, TACAS and WSC 2017,
TACAS and FORTE 2018.
Journals:
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (2013),
Information and Computation (2017, 2018),
Journal of Logical and Algebraic Methods in Programming (2017, 2018),
Software Tools for Technology Transfer (2014, 2015, 2017) and
Theoretical Computer Science (2013, 2016, 2017).