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

Projects

• Models in Space Systems: Integration, Operation, and Networking (MISSION)
  (coordinator, MSCA RISE project, 2021-2025)
• Verified Probabilistic Verification
  (NWO Open Competition project, 2021-2024)
• Verification of Cyber-Physical Systems: Exploiting Uncertainty for Scalability
  (NWO VENI personal grant, 2018-2021)

Committees

• SNR 2021 program committee member
• QEST 2021 artifact evaluation committee chair
• FORMATS 2021 program committee member
• SPIN 2021 program committee member
• SBMF 2020 program committee member
• FORMATS 2020 program committee member
• QEST 2020 program committee member
• TACAS 2020 artifact evaluation committee chair
• SETTA 2019 program committee member
• QEST 2019 program committee member
• FORTE 2018 program committee member
• TACAS 2018 artifact evaluation committee chair
• ACSD 2017 program committee member

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).