Publications

Preprints

• CLEVER: A Curated Benchmark for Formally Verified Code Generation

  A. Thakur, J. Lee, G. Tsoukalas, M. Sistla, M. Zhao, S. Zetzsche, G. Durrett, Y. Yue, S. Chaudhuri
  

  arXiv · pdf · 2025

Conferences

• Verified Foundations for Differential Privacy

  M. Medeiros, M. Naveed, T. Lepoint, T. Kahsai, T. Ravitch, S. Zetzsche, A. Joshi, J. Tassarotti, A. Albarghouthi, J. Tristan
  

  PLDI · arXiv · 2025

• Compiler Fuzzing in Continuous Integration: a Case Study on Dafny

  K. Boonriong, S. Zetzsche, A. F. Donaldson
  

  ICST · pdf · 2025

• Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny

  S. Zetzsche, W. Różowski
  

  ICTAC · arXiv · pdf · 2024

• Generators and Bases for Monadic Closures

  S. Zetzsche, A. Silva, M. Sammartino
  

  CALCO · arXiv · pdf · 2023

• Guarded Kleene Algebra with Tests: Automata Learning

  S. Zetzsche, A. Silva, M. Sammartino
  

  MFPS · arXiv · pdf · 2022

• Canonical Automata via Distributive Law Homomorphisms

  S. Zetzsche, G. v. Heerdt, M. Sammartino, A. Silva
  

  MFPS · arXiv · pdf · 2021

Workshops

• Verifying the Fisher-Yates Shuffle Algorithm in Dafny

  S. Zetzsche, T. Lepoint, J. Tristan, M. Mayer
  

  POPL (Dafny) · arXiv · 2025

• Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny

  S. Zetzsche, W. Różowski
  

  POPL (Dafny) · 2025

• Dafny as Verification-Aware Intermediate Language for Code Generation

  Y. C. Li, S. Zetzsche, S. Somayyajula
  

  POPL (Dafny) · arXiv · 2025

• Randomised Testing of the Dafny Compiler: Into the CI

  K. Boonriong, A. F. Donaldson, S. Zetzsche
  

  POPL (Dafny) · 2025

• VMC: a Dafny Library for Verified Monte Carlo Algorithms

  F. Zaiser, S. Zetzsche, J. Tristan
  

  POPL (Dafny) · 2024

Theses

• Canonical Algebraic Generators in Automata Learning

  PhD Thesis
  

  University College London · arXiv · pdf · 2023

• Generalised Duality Theory for Monoidal Categories

  MSc Thesis
  

  University of Hamburg · arXiv · pdf · 2018

• Isomorphism Classes of Vertex-Transitive Tournaments

  BSc Thesis
  

  University of Hamburg · arXiv · pdf · 2016

Blog posts

• Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny

  S. Zetzsche, W. Różowski
  

  Dafny Blog · 2024

• Cracking the Coding Interview in Dafny: Permutations

  S. Zetzsche
  

  Dafny Blog · pdf · 2023