Publications

Conferences

• 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
  

  Conference on Neural Information Processing Systems (NeurIPS) · 2025

• 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
  

  Conference on Programming Language Design and Implementation (PLDI) · Distinguished Artifact Award · 2025

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

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

  International Conference on Software Testing, Verification and Validation (ICST) · 2025

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

  S. Zetzsche, W. Różowski
  

  International Colloquium on Theoretical Aspects of Computing (ICTAC) · 2024

• Generators and Bases for Monadic Closures

  S. Zetzsche, A. Silva, M. Sammartino
  

  Conference on Algebra and Coalgebra in Computer Science (CALCO) · 2023

• Guarded Kleene Algebra with Tests: Automata Learning

  S. Zetzsche, A. Silva, M. Sammartino
  

  Conference on the Mathematical Foundations of Programming Semantics (MFPS) · 2022

• Canonical Automata via Distributive Law Homomorphisms

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

  Conference on the Mathematical Foundations of Programming Semantics (MFPS) · 2021

Workshops

• ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis

  M. Bakšys, S. Zetzsche, O. Bouissou, S. Kong, R. Delmas
  

  Dafny Workshop at the Symposium on Principles of Programming Languages (POPL) · 2026

• MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification

  M. Bakšys, S. Zetzsche, O. Bouissou
  

  Dafny Workshop at the Symposium on Principles of Programming Languages (POPL) · 2026

• DafnyPro: LLM-Assisted Automated Verification for Dafny Programs

  D. Banerjee, O. Bouissou, S. Zetzsche
  

  Dafny Workshop at the Symposium on Principles of Programming Languages (POPL) · 2026

• 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
  

  AI for Math Workshop at the International Conference on Machine Learning (ICML) · 2025

• Verifying the Fisher-Yates Shuffle Algorithm in Dafny

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

  Dafny Workshop at the Symposium on Principles of Programming Languages (POPL) · 2025

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

  S. Zetzsche, W. Różowski
  

  Dafny Workshop at the Symposium on Principles of Programming Languages (POPL) · 2025

• Dafny as Verification-Aware Intermediate Language for Code Generation

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

  Dafny Workshop at the Symposium on Principles of Programming Languages (POPL) · 2025

• Randomised Testing of the Dafny Compiler: Into the CI

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

  Dafny Workshop at the Symposium on Principles of Programming Languages (POPL) · 2025

• VMC: a Dafny Library for Verified Monte Carlo Algorithms

  F. Zaiser, S. Zetzsche, J. Tristan
  

  Dafny Workshop at the Symposium on Principles of Programming Languages (POPL) · 2024

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 · 2023