Talks
-
03 February 2025: How Commutativity Simplifies Proofs of Concurrent Programs
IRIF
Paris, France
Verification of concurrent programs over infinite data domains is challenging: Algorithmic verifiers must infer inductive invariants that show correctness for all possible interleavings of program statements. 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.
-
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 invariant-based 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
SV-COMP@ETAPS
Luxembourg, Luxembourg
I presented the algorithmic verifier GemCutter, which integrates commutativity-based reasoning and partial order abstraction algorithms with a counterexample-guided 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 thread-modular reasoning with ghost variables.
-
24 April 2023: Ultimate GemCutter
SV-COMP@ETAPS
Paris, France
I presented the algorithmic verifier GemCutter, which integrates commutativity-based reasoning and partial order abstraction algorithms with a counterexample-guided 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 abstraction-refinement 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
SV-COMP@ETAPS
Munich, Germany
I presented the software model checker Ultimate GemCutter, which combines the verification algorithm trace abstraction refinement with commutativity-based 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 language-independent 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 Self-Organising 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 self-organising systems.
