Symbolic Execution Traces Close LLM Violation Detection Gap — 14 Models Tested on 500 C Tasks

arXiv·high signalXBlueskyLinkedInCopy link

Evaluation framework of 500 C verification tasks across five property types (memory safety, overflow, termination, reachability, data races) built on SV-COMP 2025 reveals that high accuracy masks a critical weakness: models reliably confirm properties hold but violation detection varies widely and degrades with program length. Training on formal verification artifacts from the Soteria symbolic executor significantly closes this gap. Directly applicable to AI-assisted code review pipelines.