We are happy to present Dominik Klumpp’s talk titled “How Commutativity Simplifies Proofs of Concurrent Programs”.
To verify concurrent programs with unbounded loops, algorithmic verifiers must infer inductive invariants that show correctness for all infinitely many possible executions of the program. Due to the many possible interleavings of the program’s threads, such invariants are often complex (requiring non-linear arithmetic, quantifiers, or reasoning with ghost variables) and out-of-reach for most invariant inference algorithms.
In this talk, I present a series of works investigating how the notion of commutativity simplifies proofs of concurrent programs and thereby empowers algorithic verification. The idea of commutativity is based on the observation that some program statements can be reordered without affecting the outcome of an execution, and hence it suffices to verify a suitably-chosen subset of interleavings (rather than all interleavings) to conclude correctness of an entire concurrent program. We will see how commutativity-based combinatorial algorithms interact with symbolic reasoning over variables with infinite domains, and how commutativity can both extend the theoretical expressiveness and contribute to the practical success of verification approaches.
Dominik Klumpp is a PhD candidate at the University of Freiburg. He received a BSc degree in Computer Science from the University of Augsburg and a MSc degree in Software Engineering as part of a joint programme by the Technical University of Munich, LMU Munich and the University of Augsburg. For his Master thesis, he visited the group of Prof. Franck Cassez at Macquarie University, Sydney, for six months to work on provably correct control flow reconstruction from assembler code.
During his PhD at the University of Freiburg, advised by Prof. Andreas Podelski, he has focused on automated verification of concurrent programs using techniques based on the principles of commutativity and partial order reduction. His automated verification tool Ultimate GemCutter has scored top rankings in the “ConcurrencySafety” category of the International Competitions on Software Verification (SV-COMP) 2022-2025.