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,…