Dominik Klumpp
PhD Candidate, University of Freiburg
I work at the Chair for Software Engineering.
My PhD advisor is Prof. Andreas Podelski.
My main research focus is on algorithmic verification of concurrent programs. I investigate 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.
I am a co-developer of the Ultimate program analysis and automata theory framework. To complement my theoretical work on commutativity in program verification, I implement the resulting verification algorithms in the software model checker Ultimate GemCutter, which has scored top rankings in the International Competition on Software Verification (SV-COMP) 2022 and 2023.
Recent & Upcoming Talks
- 17 Jul 2023: Concurrency Correctness Witnesses with Ghosts at CAV (Paris, France)
- 24 Apr 2023: Ultimate GemCutter at ETAPS (Paris, France)
- 18 Jan 2023: Stratified Commutativity in Verification Algorithms for Concurrent Programs at POPL (virtual)
- 20 Oct 2022: Commutativity in Concurrent Program Verification at FMCAD (Trento, Italy)
Selected Publications
-
POPL’24 Commutativity Simplifies Proofs of Parameterized Programs (to appear)
-
POPL’23 Stratified Commutativity in Verification Algorithms for Concurrent Programs
-
PLDI’22 Sound Sequentialization for Concurrent Program Verification
-
WADT@ETAPS’20 𝕂 and KIV: Towards Deductive Verification for Arbitrary Programming Languages
