Stefan Zetzsche
where else to find them
no profile links on file
what they talk about
all 6 in the filters
where they keep going back
- Dafny3 editions2024–2026
on a stage with
all 21 in the filters
who talks about the same things
nobody close enough yet
| title | conference | date |
|---|---|---|
| MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification | Dafny 2026 | 2026-01-11 |
miniF2F gets fully translated into Dafny and a compact library of ~100 axiomatized lemmas, then run through Dafny’s SMT automation and 14 off‑the‑shelf LLMs… | ||
| DafnyPro: LLM-Assisted Automated Verification for Dafny Programs | Dafny 2026 | 2026-01-11 |
DafnyPro is an inference-time pipeline that uses LLMs (Claude Sonnet 3.5/3.7) to generate Dafny annotations while enforcing soundness with a diff-checker that… | ||
| ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis | Dafny 2026 | 2026-01-11 |
ATLAS is an automated pipeline that converts Python contest problems into complete Dafny programs by generating a fixed method signature, synthesizing… | ||
| Verified Foundations for Differential Privacy | PLDI 2025 | 2025-06-16 |
SampCert is a mechanized foundation for differential privacy written in Lean that proves correctness of sampling and DP composition and ships verified samplers… | ||
| Dafny as Verification-Aware Intermediate Language for Code Generation | Dafny 2025 | 2025-01-19 |
Prototype guides an LLM to emit Dafny as opaque IR which is verified and then compiled to Python, preserving a proof and added unit tests. The system converges… | ||
| Verifying the Fisher-Yates Shuffle Algorithm in Dafny | Dafny 2025 | 2025-01-19 |
Verified Fisher‑Yates implementation in Dafny defines a functional model on bitstreams, proves it yields each permutation with probability 1/n! for… | ||
| Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny | Dafny 2025 | 2025-01-19 |
Formalises that the denotational (language) and operational (deterministic automaton) semantics of regular expressions coincide, proving the inductive algebra… | ||
| Randomised Testing of the Dafny Compiler: Into the CI | Dafny 2025 | 2025-01-19 |
Integrates the fuzzer fuzz-d into Dafny’s CI as CompFuzzCI, running a brief per‑PR fuzzing campaign in containers, auto‑reducing and attempting bisection, and… | ||
| Day opening | Dafny 2024 | 2024-01-14 |
This session delivers logistics and a roadmap not technical results: 18 talks across five sessions, running 9:00–6:00 with 15+3 minute slots, plus Q&A and… | ||
| VMC: a Dafny Library for Verified Monte Carlo Algorithms | Dafny 2024 | 2024-01-14 |
Open-source Dafny library that provides verified Monte Carlo samplers: each sampler has a bitstream-to-value functional model, a machine-checked proof that the… | ||
| Day closing | Dafny 2024 | 2024-01-14 |
Day closing gives practical logistics and requests: organizers ask for written feedback for future conferences and topics, note a planned meetup at 6:45 at the… | ||
| nothing matches | ||