Dominik Klumpp, Dr. rer. nat. 
PostDoc Researcher, École Polytechnique, France
I am interested in the construction and verification of provably correct software systems.
My main research focus is on the algorithmic and deductive verification of concurrent programs.
I work at LIX with Prof. Constantin Enea.
Research Topics
In my PhD research, I investigated how partial order reduction and the underlying notion of commutativity enable verification algorithms to find simpler correctness proofs for concurrent programs, thereby allowing for the verification of more programs, and increasing verification efficiency. [PhD thesis] [SV-COMP@ETAPS’22] [PLDI’22] [POPL’23] [POPL’24] [CAV’25]
I am also interested in proof formalisms and correctness certificates for concurrent programs, how compact, modular certificates for verified programs increase confidence in verification results and verification tools through independent validation, and enable interoperability between automated and deductive verification approaches. [VMCAI’25] [POPL’26]
When verification uncovers bugs, it raises the question of program repair. As program specifications are often formalised in temporal logics, I investigate how to implement rational change of temporal behaviours, informed by the belief change paradigm of symbolic artificial intelligence. [NMR@KR’24] [KR’25]
Tools
To complement my theoretical work on commutativity in program verification, I implement the resulting verification algorithms in the software model checker Ultimate GemCutter. GemCutter has scored top rankings in SV-COMP, the International Competition on Software Verification (2022, 2023, 2024, 2025).
I am a co-developer of the Ultimate program analysis and automata theory framework. Our algorithmic verifier Ultimate Automizer has won 1st place in the Overall ranking of SV-COMP for four years in a row (2023, 2024, 2025, 2026).
Recent & Upcoming Talks
- 03 Nov 2025: From Commutativity to Proofs and Back Again: Reduction and Verification of Concurrent Programs at University of Freiburg (Freiburg, Germany)
- 21 Oct 2025: From Commutativity to Proofs and Back Again: Reduction and Verification of Concurrent Programs at LIX (Palaiseau, France)
- 20 May 2025: Finding Commutativity for Algorithmic Verification of Concurrent Programs at VDS/NETYS (Rabat, Morocco)
- 24 Mar 2025: How Commutativity Simplifies Proofs of Concurrent Programs at MPI-SWS (Kaiserslautern, Germany)
Selected Publications
-
PhD thesis
From Commutativity to Proofs and Back Again: Reduction and Verification of Concurrent Programs -
POPL’26 The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs
-
KR’25 Effective AGM Belief Contraction: A Journey beyond the Finitary Realm
-
POPL’24 Commutativity Simplifies Proofs of Parameterized Programs
-
PLDI’22 Sound Sequentialization for Concurrent Program Verification
-
WADT@ETAPS’20 𝕂 and KIV: Towards Deductive Verification for Arbitrary Programming Languages
Teaching Award (summer semester 2024)
I was the lecturer for the course Cyber-Physical Systems II: Program Verification in the summer semester 2024. The lecture received the Teaching Award of the Faculty of Engineering for the best Computer Science lecture in that semester, based on a ranking calculated from student evaluations.
Alpine Verification Meeting (AVM’24)
In 2024, I was an organizer of the Alpine Verification Meeting (AVM’24), an informal meeting on formal verification. For three days, we welcomed 67 attendees from the verification community in Freiburg to present recent and ongoing work, exchange ideas and get to know each other.
