Publications

During my PhD, I contributed to 10 publications across various fields. To give you a better overview, I grouped them by topic.

Venues

In case you know the conferences, this might be the interesting information for you: LICS, VMCAI, CAV, TACAS, ATVA, ICMLA, RV

There are also two journals: Hydrological Processes, Formal Methods in System Design

Topics

Safe Neural Networks (NNs)

Abstraction

With our publication [1], we were the first to introduce the idea of abstracting NNs to make them smaller for verification. We later refined this approach in [2] to use linear combinations to improve the abstraction even further.

Monitoring

Instead of verifying NNs during development, you can also monitor it during runtime to detect whether it is producing unreliable output. In [3], we provide a light-weight monitoring approach for NNs. The framework [4] is a tool to automatically generate, optimize, and evaluate NN monitors.

Explainability

In an interdisciplinary project, we developed ML approaches for predicting river temperatures in [5] and developed methods to explain their behavior. This approach was then used in [6] and evaluated from a hydrological perspective.

Formal Verification

Strategies

For some models, like Markov Decision Processes (MDPs) or Partially Observable MDPs (POMDPs), we want to describe a strategy. This strategy explains how to move within the model to achieve some goal or to maximize some reward. Typically, these strategies can take various formats. In [7], we show that one can generate decision trees (DTs) to represent the strategy and, more interestingly, that these DTs can generalize to models with a different parameterization. Similarly, we show that one can directly learn strategies for POMDPs within a special shape, an automaton, or FSC, by using automaton learning principles in [8]. I also contributed to a joint work on generating strategies for lexicographic objectives by implementing it in the modelchecker STORM [9].

Risk computation

In the paper [10], we look at a risk metric for MDPs. Usually, when people decide which action to take, they do not decide fully rationally. They try to prevent losses and misinterpret probabilities. We look at Cumulative Prospect Theory for modelling human behavior and evaluate its mathematical properties on MDPs.

References

• [1] DeepAbstract: Neural Network Abstraction for Accelerating Verification
  Pranav Ashok, Vahid Hashemi, Jan Kretinsky, Stefanie Mohr
  ATVA 2020
  
• [2] Syntactic vs Semantic Linear Abstraction and Refinement of Neural Networks
  Calvin Chau, Jan Kretinsky, Stefanie Mohr
  ATVA 2023
  
• [3] Gaussian-based Runtime Detection of Out-of-Distribution Inputs for Neural Networks
  Vahid Hashemi, Jan Kretinsky, Stefanie Mohr, Emmanouil Seferis
  RV 2021
  
• [4] Monitizer: Automating Design and Evaluation of Neural Network Monitors
  Muqsit Azeem, Marta Grobelna, Sudeep Kanav, Jan Kretinsky, Stefanie Mohr, Sabine Rieder
  CAV 2024
  
• [5] Assessment of Neural Networks for Stream-Water-Temperature Prediction
  Stefanie Mohr, Konstantina Drainas, Juergen Geist
  ICMLA 2021
  
• [6] Predicting stream water temperature with artificial neural networks based on open-access data
  Konstantina Drainas, Lisa Kaule, Stefanie Mohr, Bhumika Uniyal, Romy Wild, Juergen Geist
  Hydrological Processes, Volume 37, Issue 10, 2023
  
• [7] 1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
  Muqsit Azeem, Debraj Chakraborty, Sudeep Kanav, Jan Kretinsky, Mohammadsadegh Mohagheghi, Stefanie Mohr, Maximilian Weininger
  VMCAI 2025
  
• [8] Learning Explainable and Better Performing Representations of POMDP Strategies
  Alexander Bork, Debraj Chakraborty, Kush Grover, Jan Kretinsky, Stefanie Mohr
  TACAS 2024
  
• [9] Stochastic games with lexicographic objectives
  Krishnendu Chatterjee, Joost-Pieter Katoen, Stefanie Mohr, Maximilian Weininger, Tobias Winkler
  Formal Methods in System Design 2023
  
• [10] Risk-aware Markov Decision Processes Using Cumulative Prospect Theory
  Thomas Brihaye, Krishnendu Chatterjee, Stefanie Mohr, Maximilian Weininger
  LICS 2025