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 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.

  Slides Poster

• 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.

  Paper Slides Recording

• 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.

  Slides Supplemental Material

• 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.

  Slides

• 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.

  Paper Slides Recording

• 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.

  Slides Poster

• 14 September 2022: Commutativity in Concurrent Program Verification AVM
  

  Frauenchiemsee, Germany

  I gave a 30min talk summarizing my PhD research.

  Slides

• 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.

  Paper Slides Recording

• 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.

  Slides

• 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.

  Paper Slides

• 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.

  Paper Slides Recording

• 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.

  Paper Slides Recording

• 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.

  Paper Slides

• 10 September 2019: Automated Control Flow Reconstruction from Assembler Programs Using Trace Abstraction Refinement AVM
  

  virtual

  I presented the results of my Master thesis.

  Slides

• 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.

  Paper