Notions of Behavioral Equivalence
Behavioral equivalences are at the basis of program semantics in formal methods. But there’s a lot of such notions.
My research is about making the spectrum of behavioral equivalences easily usable through algorithms and tools.
Weak Behavioral Equivalences
For models with internal behavior, one usually uses so-called weak notions of equivalence that abstract away “internal” aspects.
My research interest lies with the weakest forms of bisimilarity, namely coupled similarity and contrasimilarity.
Causality and Event Structures
Often one does not only want to model what may happen in a system but also the dependencies and causalities between events.
I take particular interest in counterfactuals—a formal way of capturing what would need to change in order for statements to be true.
Real-Time Systems
Real-world systems and distributed algorithms rely heavily on concepts of real-time and timeouts.
At the beginning of my studies, I was concerned with the translation of Timed CSP to Timed Automata.
Distributed Algorithms
Distributed algorithms are at the core of our networked world.
I’ve contributed to Isabelle/HOL formalizations of distributed consensus algorithms (and of the impossibility of asynchronous consensus with faulty processes).
Functional Programming and Verification
A lot of elegance and robustness can be achieved by expressing programs mathematically.
I love using Scala for my programming and Isabelle/HOL for formal verifications and also teach the use of such tools.
Software Engineering
At the end of the day, we’re all software engineers.
I give courses touching upon Scrum project management, object-oriented programming, game dev, and quality assurance.
2024
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2011
2010
Accelerating Process Equivalence Energy Games using WebGPU
MTV TU Berlin
(2024-04)
Accelerating Process Equivalence Energy Games using WebGPU
Measuring expressive power of HML formulas in Isabelle/HOL
MTV TU Berlin
(2024-04)
Measuring expressive power of HML formulas in Isabelle/HOL
Write, Review, and Publish (Master seminar)
MTV TU Berlin
(2024-04)
Write, Review, and Publish (Master seminar)
Course
Concurrency Formalisms as Games
D-CON 2024, Oldenburg
(2024-02)
Concurrency Formalisms as Computer Games
Talk
Integration eines generischen Äquivalenzprüfers in CAAL
MTV TU Berlin
(2023-10)
Integration eines generischen Äquivalenzprüfers in CAAL
Process Equivalence Problems as Energy Games
CAV'23, LNCS 13964
(2023-08)
Process Equivalence Problems as Energy Games
Games to Decide All Behavioral Equivalences
HIGHLIGHTS'23, Kassel
(2023-07)
Games to Decide All Behavioral Equivalences at Once
Process Equivalence Problems as Energy Games
CAV 2023, Paris
(2023-07)
Process Equivalence Problems as Energy Games
Talk
Energy games to navigate the landscape of equivalences
LFCS University of Edinburgh
(2023-03)
Energy games to navigate the landscape of behavioural equivalences
Talk
Coupled Similarity and Contrasimilarity, and How to Compute Them
AFP 2023
(2023-08)
Coupled Similarity and Contrasimilarity, and How to Compute Them
Artifact
Linear-Time–Branching-Time Spectroscopy Accounting for Silent...
arXiv
(2023-05)
Linear-Time–Branching-Time Spectroscopy Accounting for Silent Steps
Paper
Nonlinear Counterfactuals in Isabelle/HOL
MTV TU Berlin
(2023-12)
Nonlinear Counterfactuals in Isabelle/HOL
Computer game about counterfactual truth conditions
MTV TU Berlin
(2023-01)
An educational computer game about counterfactual truth conditions
Research at Work (Master project course)
MTV TU Berlin
(2023-10)
Research at Work (Master project course)
Course
Deciding All Behavioral Equivalences at Once
Deciding All Behavioral Equivalences at Once: A Game for Linear-Time–Branching-Time Spectroscopy
Article
An educational tool for Linear-time–Branching-time Spectroscopy
MTV TU Berlin
(2022-07)
Developing an educational tool for Linear-time–Branching-time Spectroscopy
A Video Game about Reactive Bisimilarity
MTV TU Berlin
(2022-12)
A Video Game about Reactive Bisimilarity
Automatisierte Reduktion von reaktiver zu starker Bisimilarität
MTV TU Berlin
(2022-11)
Automatisierte Reduktion von reaktiver zu starker Bisimilarität
Simulation fehlertoleranter Konsensalgorithmen in Hash.ai
MTV TU Berlin
(2022-11)
Simulation fehlertoleranter Konsensalgorithmen in Hash.ai
Advising
Supervisors: Uwe Nestmann, Stefan Schmid
HML Synthesis of Distinguished Processes
MTV TU Berlin
(2021-12)
HML Synthesis of Distinguished Processes
Linear-Time−Branching-Time Spectroscopy as an Educational Web...
MTV TU Berlin
(2021-11)
Linear-Time−Branching-Time Spectroscopy as an Educational Web Browser Game
Let's decide all equivalences at once!
Student Session VTSA 2021
(2021-10)
Let's decide all equivalences at once!
Talk
Video: A Game for Linear-time–Branching-time Spectroscopy
TACAS 2021, Morressier
(2021-03)
Video: A Game for Linear-time–Branching-time Spectroscopy
A Game for Linear-time–Branching-time Spectroscopy
TACAS 2021, LNCS 12651
(2021-03)
A Game for Linear-time–Branching-time Spectroscopy
Paper
Linear-time–Branching-time Spectroscope TACAS'21 Edition
Zenodo
(2021-01)
Linear-time–Branching-time Spectroscope: TACAS 2021 Edition
Artifact
A Game Characterization for Contrasimilarity
EXPRESS/SOS 2021, EPTCS 339
(2021-08)
A Game Characterization for Contrasimilarity
Paper
Reducing Strong Reactive Bisimilarity to Strong Bisimilarity
MTV TU Berlin
(2021-06)
Reducing Strong Reactive Bisimilarity to Strong Bisimilarity
Introduction into interactive theorem proving (Isabelle-Lab)
MTV TU Berlin
(2021-09)
Introduction into interactive theorem proving (Isabelle-Lab)
Course
Statically analysing Elixir programs
MTV TU Berlin
(2021-01)
Statically analysing inter-process communication in Elixir programs
Advising
Supervisors: Uwe Nestmann, Florian Kammüller
Charting the jungle of process calculi encodings
MTV TU Berlin
(2020-12)
Charting the jungle of process calculi encodings
Advising
Supervisors: Uwe Nestmann, Kirstin Peters
Spiel zu Verhaltensäquivalenzen
MTV TU Berlin
(2020-09)
Ein Computerspiel zum Erlernen von Verhaltensäquivalenzen
Advising
Supervisors: Uwe Nestmann, Manfred Hauswirth
Coupled Similarity: The First 32 Years
Acta Informatica 57(3)
(2020-10)
Coupled Similarity: The First 32 Years
Article
Coupled Similarity as an automated checker for mCRL2
MTV TU Berlin
(2020-05)
Implementing Coupled Similarity as an automated checker for mCRL2
Advising
Supervisors: Uwe Nestmann, Stephan Kreutzer
Process equivalences as a video game
MTV TU Berlin
(2020-05)
Process equivalences as a video game
Advising
Supervisors: Uwe Nestmann, Manfred Hauswirth
Visualising and Model Checking Counterfactuals
MTV TU Berlin
(2020-09)
Visualising and Model Checking Counterfactuals
Advising
Supervisors: Uwe Nestmann, Stephan Kreutzer
Counterfactuals, Dispositions, and Hyperproperties
D-CON 2020
(2020-03)
Counterfactuals, Dispositions, and Hyperproperties
Talk
Introduction into interactive theorem proving (Isabelle-Lab)
MTV TU Berlin
(2020-09)
Introduction into interactive theorem proving (Isabelle-Lab)
Course
Isabelle/HOL proof and Apache Flink program for TACAS 2019 paper
Figshare
(2019-03)
Isabelle/HOL proof and Apache Flink program for TACAS 2019 paper
Artifact
Introduction into interactive theorem proving (Isabelle-Lab)
MTV TU Berlin
(2019-08)
Introduction into interactive theorem proving (Isabelle-Lab)
Course
Computing Coupled Similarity
TU Berlin
(2018-04)
Computing Coupled Similarity
Master thesis
Supervisors: Uwe Nestmann, Holger Hermanns
Computing Coupled Similarity – When Weak Bisimulation Is Too ...
D-CON 2018, Darmstadt
(2018-03)
Computing Coupled Similarity – When Weak Bisimulation Is Too Strong
Talk
Event Structures with Higher-Order Dynamics
TU Berlin
(2017-12)
Event Structures with Higher-Order Dynamics
Contribution to work by
Tooltorial for HD-Event Structures
D-CON 2017, Paderborn
(2017-03)
Tooltorial for HD-Event Structures
Talk
HDES Tool – Analyzing Higher-order Dynamic-causality Event St...
DFG Graduiertenkolleg SOAMED
(2016-07)
HDES Tool – Analyzing Higher-order Dynamic-causality Event Structures
Tool
Supervisor: David S. Karcher
Mechanical Verification of a Constructive Proof for FLP
ITP 2016, LNCS 9807
(2016-08)
Mechanical Verification of a Constructive Proof for FLP
Paper
Analysis and implementation of hierarchical mutually recursiv...
(2015-10)
Analysis and implementation of hierarchical mutually recursive first class modules
Contribution to work by
Implementing Control Flow Analysis for a Functional Language ...
TU Berlin
(2014-04)
Implementing Control Flow Analysis for a Functional Language with First-Class Modules
Bachelor thesis
Supervisors: Peter Pepper, Stefan Jähnichen
Modeling and verification of distributed algorithms in theore...
TU Berlin
(2013-09)
Modeling and verification of distributed algorithms in theorem proving environments
Contribution to work by
Exercise: Algorithmic and functional solution of discrete pro...
SESE TU Berlin
(2013-10)
Exercise: Algorithmic and functional solution of discrete problems
Course
Supervisor: Sabine Glesner
Exercise: Data structures and algorithms in imperative progra...
CG TU Berlin
(2013-04)
Exercise: Data structures and algorithms in imperative programming
Course
Supervisor: Marc Alexa
Mechanical Verification of Parameterized Real-Time Systems
SESE TU Berlin
(2012-05)
Mechanical Verification of Parameterized Real-Time Systems
Contribution to work by
Exercise: Algorithmic and functional solution of discrete pro...
ÜBB TU Berlin
(2012-10)
Exercise: Algorithmic and functional solution of discrete problems
Course
Supervisor: Peter Pepper
Exercise: Data structures and algorithms in imperative progra...
RBO TU Berlin
(2012-04)
Exercise: Data structures and algorithms in imperative programming
Course
Supervisor: Oliver Brock
tcsp2ta: Automatic translation of Timed CSP to Timed Automata
DFG Project VATES
(2011-05)
tcsp2ta: Automatic translation of Timed CSP to Timed Automata
Tool
Supervisors: Thomas Göthel, Sabine Glesner
Exercise: Algorithmic and functional solution of discrete pro...
SESE TU Berlin
(2011-10)
Exercise: Algorithmic and functional solution of discrete problems
Course
Supervisor: Sabine Glesner
Exercise: Data structures and algorithms in imperative progra...
RBO TU Berlin
(2011-04)
Exercise: Data structures and algorithms in imperative programming
Course
Supervisor: Oliver Brock
Exercise: Algorithmic and functional solution of discrete pro...
ÜBB TU Berlin
(2010-10)
Exercise: Algorithmic and functional solution of discrete problems
Course
Supervisor: Peter Pepper