2 citations · 3 across the 3 of their papers we have counts for
4 papers
DafnyPro: LLM-Assisted Automated Verification for Dafny Programs
Debangshu Banerjee, Olivier Bouissou, Stefan Zetzsche
We present DafnyPro, an inference-time framework that enhances LLMs for generating verification annotations in Dafny. DafnyPro comprises three key components: a diff-checker that p…
ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
Mantas Baksys, Stefan Zetzsche, Olivier Bouissou +3
Large language models have become proficient at generating functional code, but ensuring the output truly matches the programmer's intent remains difficult. Testing improves trust,…
CLEVER: A Curated Benchmark for Formally Verified Code Generation
Amitayush Thakur, Jasper Lee, George Tsoukalas +6
We introduce , a high-quality, curated benchmark of 161 problems for end-to-end verified code generation in Lean. Each problem consists of (1) the task of ge…
Dafny as Verification-Aware Intermediate Language for Code Generation
Yue Chen Li, Stefan Zetzsche, Siva Somayyajula
Using large language models (LLMs) to generate source code from natural language prompts is a popular and promising idea with a wide range of applications. One of its limitations i…