Journal articles and formalizations

2025-11
AFP 2025
The Weak Spectroscopy Game to Characterize Behavioral Equivalences
Lisa Barthel, Leonard Hübner, Caroline Lemke, Karl Mattes, Lenard Mollenkopf, Benjamin Bisping
2024-07
Information and Computation
Characterizing Contrasimilarity through Games, Modal Logic, and Complexity
Benjamin Bisping, Luisa Montanari
2023-08
AFP 2023
Coupled Similarity and Contrasimilarity, and How to Compute Them
Benjamin Bisping, Luisa Montanari
2022-08
Logical Methods in Computer Science 18(3)
Deciding All Behavioral Equivalences at Once: A Game for Linear-Time–Branching-Time Spectroscopy
Benjamin Bisping, David N. Jansen, Uwe Nestmann
2020-10
Acta Informatica 57(3)
Coupled Similarity: The First 32 Years
Benjamin Bisping, Uwe Nestmann, Kirstin Peters
2016-05
AFP 2016
A Constructive Proof for FLP
Benjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stüber, Arno Wilhelm-Weidner, Kirstin Peters, Uwe Nestmann

Conference papers

2025-09
CONCUR 2025, LIPIcs 348
Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems
Caroline Lemke, Benjamin Bisping
2024-11
EPTCS 412 of EXPRESS/SOS 2024
One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics
Benjamin Bisping, David Jansen
2023-08
CAV'23, LNCS 13964
Process Equivalence Problems as Energy Games
Benjamin Bisping
2021-08
EXPRESS/SOS 2021, EPTCS 339
A Game Characterization for Contrasimilarity
Benjamin Bisping, Luisa Montanari
2021-03
TACAS 2021, LNCS 12651
A Game for Linear-time–Branching-time Spectroscopy
Benjamin Bisping, Uwe Nestmann
2019-04
TACAS 2019, LNCS 11427
Computing Coupled Similarity
Benjamin Bisping, Uwe Nestmann
2016-08
ITP 2016, LNCS 9807
Mechanical Verification of a Constructive Proof for FLP
Benjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stüber, Arno Wilhelm-Weidner, Kirstin Peters, Uwe Nestmann

Talks

2025-12
Lehrerfortbildung in Informatik, Dagstuhl
Paradoxien einfach lösen mit interaktiven Theorembeweisern
2025-08
RADICAL, Aarhus
Generalized Equivalence Checking of Concurrent Programs
2025-07
BEL 301, Villa Bell, TU Berlin
Thesis Defense: Generalized Equivalence Checking of Concurrent Programs
(Supervisors: Rob van Glabbeek, Jan Friso Groote, Uwe Nestmann)
2025-06
P-ACTS, Paris
Deciding All Behavioral Equivalences at Once through Energy Games
2025-03
D-CON 2025, Augsburg
Deciding All Behavioral Equivalences at Once through Energy Games
2024-09
ISCAS, Beijing
Equivalence Problems as Games
2024-09
EXPRESS/SOS 2024 @ CONCUR, Calgary
One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics
2024-02
D-CON 2024, Oldenburg
Concurrency Formalisms as Computer Games
2023-07
HIGHLIGHTS'23, Kassel
Games to Decide All Behavioral Equivalences at Once
2023-07
CAV 2023, Paris
Process Equivalence Problems as Energy Games
2023-03
LFCS University of Edinburgh
Energy games to navigate the landscape of behavioural equivalences
2021-10
Student Session VTSA 2021
Let's decide all equivalences at once!
Benjamin Bisping
2021-03
TACAS 2021, Morressier
Video: A Game for Linear-time–Branching-time Spectroscopy
Benjamin Bisping
2020-03
D-CON 2020
Counterfactuals, Dispositions, and Hyperproperties
2019-04
TACAS 2019, Prague
Computing Coupled Similarity
2018-03
D-CON 2018, Darmstadt
Computing Coupled Similarity – When Weak Bisimulation Is Too Strong
2017-12
Depend Uni Saarland
Coupled Similarity
2017-03
D-CON 2017, Paderborn
Tooltorial for HD-Event Structures
Benjamin Bisping, Paul-David Brodmann, David S. Karcher

Software and artifacts

2023-01
X-mas project
MD Basic
2022-07
TU Berlin
pr.mtv.tu-berlin.de
2021-07
concurrency-theory.org
Benjamin Bisping, Pedro D’Argenio
2020-08
Linear-time–Branching-time Spectroscope
2018-02
Coupled Sim Fiddle
2016-07
DFG Graduiertenkolleg SOAMED
HDES Tool – Analyzing Higher-order Dynamic-causality Event Structures
(Supervisor: David S. Karcher)
2013-07
ÜBB TU Berlin
SL2 Module System
Benjamin Bisping, Rico Jasper, Sebastian Lohmeier, Friedrich Psiorz (Supervisor: Christoph Höger)
2011-05
DFG Project VATES
tcsp2ta: Automatic translation of Timed CSP to Timed Automata
(Supervisors: Thomas Göthel, Sabine Glesner)

Courses taught

2025-04
Models of Dynamic Systems
2024-05
Models of Dynamic Systems
2024-04
Write, Review, and Publish (Master seminar)
2023-10
Research at Work (Master project course)
2023-04
Models of Dynamic Systems
2022-10
The Software Horror Picture Show
2022-04
Models of Dynamic Systems
2021-10
The Software Horror Picture Show
2021-09
Introduction into interactive theorem proving (Isabelle-Lab)
Florian Kammüller, Benjamin Bisping
2021-04
Models of Dynamic Systems
2020-10
Models of Dynamic Systems
2020-09
Introduction into interactive theorem proving (Isabelle-Lab)
Florian Kammüller, Benjamin Bisping
2020-04
Models of Dynamic Systems
2019-10
Models of Dynamic Systems
2019-08
Introduction into interactive theorem proving (Isabelle-Lab)
Florian Kammüller, Benjamin Bisping
2019-04
Models of Dynamic Systems
2018-10
Models of Dynamic Systems
Benjamin Bisping, Uwe Nestmann
2013-10
Exercise: Algorithmic and functional solution of discrete problems
(Supervisor: Sabine Glesner)
2013-04
Exercise: Data structures and algorithms in imperative programming
(Supervisor: Marc Alexa)
2012-10
Exercise: Algorithmic and functional solution of discrete problems
(Supervisor: Peter Pepper)
2012-04
Exercise: Data structures and algorithms in imperative programming
(Supervisor: Oliver Brock)
2011-10
Exercise: Algorithmic and functional solution of discrete problems
(Supervisor: Sabine Glesner)
2011-04
Exercise: Data structures and algorithms in imperative programming
(Supervisor: Oliver Brock)
2010-10
Exercise: Algorithmic and functional solution of discrete problems
(Supervisor: Peter Pepper)

Theses supervised

2025-07
Automating Legal Reasoning in Isabelle/HOL: An Embedding of Logics for Legal Dynamics
Eric Lifante (Supervisors: Uwe Nestmann, Christoph Benzmüller)
2025-06
User-Friendly Web Application for High-Performance Process Equivalence Checking
Finn Watermann (Supervisors: Uwe Nestmann, David N. Jansen)
2024-11
A Formal Proof of Decidability of Multi-Weighted Declining Energy Games
Caroline Lemke (Supervisors: Uwe Nestmann, Uli Fahrenberg)
2024-11
Implementierung eines Contrasimilarity-Checkers für mCRL2
Tilo Kurzan (Supervisors: Uwe Nestmann, Stephan Kreutzer)
2024-08
Higher-Order Diadic µ-Calculus—An Efficient Framework for Checking Process Equivalences?
Valentin Stöcker (Supervisors: Uwe Nestmann, Martin Lange)
2024-04
Accelerating Process Equivalence Energy Games using WebGPU
Gabriel Vogel (Supervisors: Uwe Nestmann, Stephan Kreutzer)
2024-04
Measuring expressive power of HML formulas in Isabelle/HOL
Karl Mattes (Supervisors: Uwe Nestmann, Stephan Kreutzer)
2023-12
Nonlinear Counterfactuals in Isabelle/HOL
Johannes Hauschild (Supervisors: Uwe Nestmann, Bernd Finkbeiner)
2023-10
Integration eines generischen Äquivalenzprüfers in CAAL
Fabian Ozegowski (Supervisors: Uwe Nestmann, Stephan Kreutzer)
2023-01
An educational computer game about counterfactual truth conditions
Bruno Lönne (Supervisors: Uwe Nestmann, Stephan Kreutzer)
2022-12
A Video Game about Reactive Bisimilarity
Eloi Sandt (Supervisors: Uwe Nestmann, Stephan Kreutzer)
2022-11
Simulation fehlertoleranter Konsensalgorithmen in Hash.ai
Roy Adler (Supervisors: Uwe Nestmann, Stefan Schmid)
2022-11
Automatisierte Reduktion von reaktiver zu starker Bisimilarität
Zead Alshukairi (Supervisors: Uwe Nestmann, Stephan Kreutzer)
2022-07
Developing an educational tool for Linear-time–Branching-time Spectroscopy
Thanh Mai Duong (Supervisors: Uwe Nestmann, Stephan Kreutzer)
2021-12
HML Synthesis of Distinguished Processes
Johanna England (Supervisors: Uwe Nestmann, Stephan Kreutzer)
2021-11
Linear-Time−Branching-Time Spectroscopy as an Educational Web Browser Game
Mariusz Trzeciakiewicz (Supervisors: Uwe Nestmann, Stephan Kreutzer)
2021-06
Reducing Strong Reactive Bisimilarity to Strong Bisimilarity
Maximilian Pohlmann (Supervisors: Uwe Nestmann, Stephan Kreutzer)
2021-05
Kontrasimulation als Spiel
Luisa Montanari (Supervisors: Uwe Nestmann, Stephan Kreutzer)
2021-01
Statically analysing inter-process communication in Elixir programs
Jonas Bulik (Supervisors: Uwe Nestmann, Florian Kammüller)
2020-12
Charting the jungle of process calculi encodings
Tobias Wittig (Supervisors: Uwe Nestmann, Kirstin Peters)
2020-09
Visualising and Model Checking Counterfactuals
Jannik Moritz Reichert (Supervisors: Uwe Nestmann, Stephan Kreutzer)
2020-09
Ein Computerspiel zum Erlernen von Verhaltensäquivalenzen
Michael Wrusch (Supervisors: Uwe Nestmann, Manfred Hauswirth)
2020-05
Implementing Coupled Similarity as an automated checker for mCRL2
Hùòng Ngoc Lê (Supervisors: Uwe Nestmann, Stephan Kreutzer)
2020-05
Process equivalences as a video game
Dominik Peacock (Supervisors: Uwe Nestmann, Manfred Hauswirth)