Talks

• 08 April 2024: Ultimate GemCutter SV-COMP@ETAPS
  

  Luxembourg, Luxembourg

  I will present 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.

  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