1 citations · 1 across the 4 of their papers we have counts for
4 papers · 1 filter
Teaching LLMs Program Semantics via Symbolic Execution Traces
Jonas Bayer, Stefan Zetzsche, Olivier Bouissou +3
We introduce an evaluation framework of 500 C verification tasks across five property types (memory safety, overflow, termination, reachability, data races) built on SV-COMP 2025,…
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,…
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…
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…