AutoFraming (arXiv:2610.29046v1): LLMs synthesize ACSL frame specifications for C code
The AutoFraming preprint proposes an LLM-based method that, guided by code property graphs (CPGs), synthesizes ACSL frame specifications alongside functional contracts for C functions. On two real-world benchmarks (84 and 51 ACSL-compliant functions) it reports error-free frame-spec synthesis rates of 92.9% (179% relative improvement over prior work) and 96.1% (up from 80.4%), and when used as an auxiliary component it can boost existing frameworks’ frame-generation performance by up to 61.9%.