ORCID dblp Scholar ResearchGate Uni Freiburg LinkedIn Mastodon

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 SV-COMP, the International Competition on Software Verification (2022, 2023, 2024, 2025).

I am also part of the development team for Ultimate Automizer. Our team has won 1st place in the Overall ranking of SV-COMP for three years in a row (2023, 2024, and 2025).

Recent & Upcoming Talks

Selected Publications

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.

Dominik Klumpp