4 papers
MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification
Mantas Baksys, Stefan Zetzsche, Olivier Bouissou +1
LLMs excel at reasoning, but validating their steps remains challenging. Formal verification offers a solution through mechanically checkable proofs. Interactive theorem provers (I…
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…