Talks

14 May 2024: How Commutativity Simplifies Proofs of Concurrent Programs ISTA
Klosterneuburg, Austria
Verification of concurrent programs is a hard problem. Beyond the state space explosion known from model checking, a new challenge arises for invariantbased verification of concurrent programs over infinite data domains: the inductive invariants needed to prove correctness of all possible program interleavings are often complex and out of reach for automated invariant inference algorithms. In this talk, I will present several recent works investigating how commutativity simplifies such proofs of concurrent programs. The notion of commutativity is based on the observation that some statements can be reordered without affecting the outcome of an execution and it suffices to verify a suitably chosen subset of interleavings to conclude the correctness of an entire concurrent program. I will discuss how commutativity reasoning can extend the theoretical expressiveness of verification approaches, in which cases commutativity makes the difference between finding a proof and never terminating, and how symbolic reasoning (over variables with infinite domain) interacts with commutativity.

08 April 2024: Ultimate GemCutter SVCOMP@ETAPS
Luxembourg, Luxembourg
I presented the algorithmic verifier GemCutter, which integrates commutativitybased reasoning and partial order abstraction algorithms with a counterexampleguided abstraction refinement verification algorithm based on trace abstraction.

17 January 2024: Commutativity Simplifies Proofs of Parameterized Programs POPL
London, UK
I presented our paper on how commutativity reasoning can simplify proofs of parameterized programs, in the sense that less complex ghost state is needed.

17 July 2023: Concurrency Correctness Witnesses with Ghosts VeWit@CAV
Paris, France
Frank Schüssele presented our work on concurrency correctness witnesses based on threadmodular reasoning with ghost variables.

24 April 2023: Ultimate GemCutter SVCOMP@ETAPS
Paris, France
I presented the algorithmic verifier GemCutter, which integrates commutativitybased reasoning and partial order abstraction algorithms with a counterexampleguided abstraction refinement verification algorithm based on trace abstraction.

18 January 2023: Stratified Commutativity in Verification Algorithms for Concurrent Programs POPL
virtual
I presented our paper on how abstract commutativity and the stratified combination of commutativity relations can be used in algorithmic verification.

20 October 2022: Commutativity in Concurrent Program Verification FMCAD
Trento, Italy
I gave a short talk and presented a poster summarizing my PhD research, as part of the FMCAD student forum.

14 September 2022: Commutativity in Concurrent Program Verification AVM
Frauenchiemsee, Germany
I gave a 30min talk summarizing my PhD research.

16 June 2022: Sound Sequentialization for Concurrent Program Verification PLDI
San Diego, USA
I presented our paper on how commutativity can be used to simplify proofs and increase proof checking efficiency in an abstractionrefinement based verification algorithm.

14 June 2022: Extending Commutativity via Safe Abstraction Commute@PLDI
San Diego, USA
I presented ongoing work on how “safe” abstraction can change and extend the commutativity available to verification algorithms.

07 April 2022: Ultimate GemCutter and the Axes of Generalization SVCOMP@ETAPS
Munich, Germany
I presented the software model checker Ultimate GemCutter, which combines the verification algorithm trace abstraction refinement with commutativitybased reasoning, in the form of partial order reduction algorithms.

17 January 2021: Verification of Concurrent Programs Using Petri Net Unfoldings VMCAI
virtual
I presented our paper on a variation of the trace abstraction refinement verification algorithm targeted at concurrent programs, and based on (bounded) Petri nets.

25 June 2020: Partial Order Reduction for Trace Abstraction Refinement MOVEP
virtual
I presented ongoing work and plans for future work as part of my PhD thesis.

29 April 2020: K and KIV – Towards Deductive Verification for Arbitrary Programming Languages WADT@ETAPS
virtual
I presented our paper on an implementation of a languageindependent program verification calculus into the interactive proof assistant KIV, and the development on a KIV frontend based on the K semantic framework.

10 September 2019: Automated Control Flow Reconstruction from Assembler Programs Using Trace Abstraction Refinement AVM
virtual
I presented the results of my Master thesis.

12 September 2016: Optimising Runtime Safety Analysis Efficiency for SelfOrganising Systems QA4SASO@SASO
Augsburg, Germany
I presented our paper on how heuristics can speed up safety analyis (i.e., analysis of robustness in the presence of hardware faults), particularly for selforganising systems.