AutoFraming: Synthesizing Dynamic Frames of C Code with LLMs

Han Zhou; Yu Luo; Dianxiang Xu

cs.AIOct 21, 2026

AutoFraming: Synthesizing Dynamic Frames of C Code with LLMs

Authors: Han Zhou, Yu Luo, Dianxiang Xu

Organizations: University of Missouri–Kansas City, Kansas City, USA · University of Central Missouri, Warrensburg, USA

Abstract

Large language models (LLMs) have shown considerable promise in synthesizing formal specifications from source code. However, existing approaches primarily focus on functional contracts and loop invariants, while largely neglecting frame conditions, which specify the memory locations that may or may not be modified during execution and constitute an essential part of formal specifications. To address this limitation, we propose an LLM-based approach for synthesizing ACSL frame specifications alongside functional contracts from C code. Our approach analyzes code property graphs (CPGs) to extract frame-relevant information from the input code and leverages this information to guide the LLM in generating accurate frame conditions. The resulting specifications capture both region-separation constraints and data dependencies that govern variable modifications. Experimental results demonstrate the effectiveness of our approach. On a benchmark of 84 ACSL-compliant functions from non-trivial real-world systems, our method successfully synthesizes error-free frame specifications for 92.9% of the functions, representing a 179% relative improvement over state-of-the-art techniques. On a second benchmark consisting of 51 functions, the success rate increases from 80.4% to 96.1%. Furthermore, when integrated as an auxiliary component into existing LLM-based ACSL-synthesis frameworks, our approach improves frame-specification generation performance by up to 61.9%.

Figures & tables

Fig. 1: AutoFraming Pipeline for CPG-guided Frame Specification Synthesis.

Component	Meaning	CPG view	Used by
$\mathcal{R}_{f}$	caller-visible roots: parameters and globals touched by $f$	AST	Sep, Dep
$\Omega_{f}$	access window of each pointer root	AST, CFG	Sep, Dep
$\mathcal{I}_{f}$	interfering pointer-root pairs requiring separation	AST, PDG	Sep
$\mathcal{L}_{f}$	normalized write-set locations used as assigns carriers	AST, CFG	Dep
$\Delta_{f}$	dependence footprint of each write set location	PDG	Dep

TABLE I: The frame-information set

\Phi_{f}

extracted from the CPG.

Program	#Fns	LOC	Preguss	AF-GPT	AF-Gemini
AES-CCM	10	610	2	6	8
Antelope memb	1	55	0	1	0
Antelope relation	1	42	0	1	1
Atomthreads	10	830	1	10	9
Contiki ctimer	10	315	0	10	10
Contiki etimer	10	195	8	10	10

TABLE II: Error-free frame counts per program on the real-world benchmark

\mathcal{D}_{\mathrm{a}}

.AF-GPT and AF-Gemini denote AutoFraming instantiated with GPT-5.2 and Gemini-2.5-Pro, respectively.

Category	#Fns	AutoSpec	Preguss	AF-GPT	AF-Gemini
arrays_and_loops	5	3	4	5	5
general_wp_problems	12	10	10	12	12
immutable_arrays	8	0	8	7	7
loops	8	1	5	8	7
miscellaneous	5	2	4	4	5
more_arrays	3	0	2	3	3

TABLE III: Error-free frame counts per category on the academic benchmark

\mathcal{D}_{\mathrm{b}}

. AF-GPT and AF-Gemini denote AutoFraming instantiated with GPT-5.2 and Gemini-2.5-Pro, respectively.

		Frame	Frame	Frame
Benchmark	Method	Warning	Fail	Error-free
$\mathcal{D}_{\mathrm{a}}$ (84)	Preguss	51	5	28
	AF-GPT	2	5	77
	AF-Gemini	4	2	78
$\mathcal{D}_{\mathrm{b}}$ (51)	AutoSpec	28	0	23
	Preguss	10	0	41

TABLE IV: Frame-outcome breakdown per method—frame warnings, frame failures, and error-free—with each row summing to #Fns. AF-GPT and AF-Gemini denote AutoFraming instantiated with GPT-5.2 and Gemini-2.5-Pro, respectively.

Configuration	#Clean	Rate
LLM Refinement Only	53/84	63.1%
Without CPG derived info	48/84	57.1%
Without frame-constrained projection	54/84	64.3%
AutoFraming	78/84	92.9%

TABLE V: RQ2: Ablation on

\mathcal{D}_{\mathrm{a}}

error-free frame counts for AutoFraming and three reduced variants.

Benchmark	Upstream	#Fns	Error-free frame	Goal-prove
$\mathcal{D}_{\mathrm{a}}$	Preguss	84	28 (33.3%)	94.0%
	Preguss+LLMRefine	84	52 (61.9%)	93.2%
	Preguss+AutoFraming	84	80 (95.2%)	96.8%
$\mathcal{D}_{\mathrm{b}}$	AutoSpec	51	23 (45.1%)	86.4%
	AutoSpec+LLMRefine	51	36 (70.6%)	89.4%
	AutoSpec+AutoFraming	51	50 (98.0%)	97.9%

TABLE VI: RQ3: error-free frame counts and goal-prove rates when AutoFraming augments existing generators. “+LLMRefine” denotes direct LLM refinement without AutoFraming’s frame-constrained projection, and “+AutoFraming” denotes refinement with AutoFraming.

Program Synthesis

Program synthesis automatically constructs executable programs from examples, specifications, demonstrations, or natural-language descriptions.

See all 182 papers

AutoACSL: Synthesizing ACSL Specifications by Integrating LLMs with CPG-Based Static Analysis
Jun 18, 2026Han Zhou, Yu Luo, Dianxiang XuFormal Verification
University of Missouri–Kansas City, Kansas City, USA · University of Central Missouri, Warrensburg, USA
Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications
Mar 12, 2026Liao Zhang, Tong Chen, Xiwei Wu +4Formal Verification Autoformalization
School of Computer Science, Shanghai Jiao Tong University · Shanghai Innovation Institute · School of Computer Science and Engineering, University of Washington +1
LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation
May 2, 2026Dong Xu, Jialun Cao, Guozhao Mo +9LLM Agent Evaluation Formal Verification
Institute of Software, Chinese Academy of Sciences · The Hong Kong University of Science and Technology · Guangzhou Institute of Technology, Xidian University

Jun 18, 2026J/K move · Enter open · S save

AutoACSL: Synthesizing ACSL Specifications by Integrating LLMs with CPG-Based Static Analysis

Han Zhou, Yu Luo, Dianxiang Xu

University of Missouri–Kansas City, Kansas City, USA · University of Central Missouri, Warrensburg, USA

Formal Verification

Open paper AskPDF arXiv

Generating formal specifications for C programs remains a challenge in formal verification due to the manual effort, expertise, and semantic precision required. While recent advancements in large language models (LLMs) offer promise in automating specification synthesis, current approaches often lack semantic depth and produce unverifiable or incomplete contracts. To address these limitations, we introduce AutoACSL, a novel framework that integrates LLM prompting with semantic features extracted from Code Property Graphs (CPGs). AutoACSL performs static analyses to extract key semantic elements, including arithmetic operations, loop and recursion structures, and return value propagation, which are encoded into structured prompts. These prompts enable the LLM not only to generate normal behavioral specifications but also to include constraints that prevent inputs leading to runtime errors. AutoACSL employs a feedback-driven synthesis loop, where candidate specifications are verified using Frama-C/WP and refined iteratively until verification succeeds or a termination condition is met. Evaluated on 604 programs drawn from diverse datasets, AutoACSL achieves a 98% specification generation success ratio and a 96% full proof ratio when paired with Gemini-3. Compared to a code-only baseline, AutoACSL improves the full proof ratio by 24.7% to 51.7% across four LLMs (GPT-o4 Mini, GPT-5.2, Grok-4.1, and Gemini-3), demonstrating that integrating large language models with CPG-based static analysis substantially enhances both generation robustness and verification effectiveness for automated ACSL specification synthesis.

Abstract

Program Synthesis

Explore similar work

AutoACSL: Synthesizing ACSL Specifications by Integrating LLMs with CPG-Based Static Analysis

Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications

LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation