一句话：构建 50 万余条经 Frama-C/WP 验证的 C/ACSL 语料与 495 个跨函数调用规约合成任务，揭示 LLM 随调用链增长性能下降。
面向 C 程序的形式规约合成是通向可扩展演绎验证的关键一步，但现有基于学习的方法既缺少大规模经过验证的 C/ACSL 数据，也缺少需要跨函数调用进行推理的评测任务。本文提出 ACSLBench，一个可复用的数据集制品，包含两部分：一是由已验证的 Rust/Verus 种子通过 LLM 引导的语义映射循环翻译得到的 504,587 个形式验证过的 C/ACSL 程序语料，其中失败的候选由 Frama-C/WP 的反馈驱动修复；二是由已验证组件合成的 495 个基准任务，其调用者函数的规约依赖多个被调用者的契约。对六个 LLM 的实验表明，随着函数调用数量的增加，规约合成性能明显下降。
Formal specification synthesis for C programs is a key step toward scalable deductive verification, yet current learning-based approaches lack large verified C/ACSL data and evaluation tasks that exercise reasoning across function calls. We present ACSLBench, a reusable dataset artifact for training and evaluating C/ACSL specification synthesis models. ACSLBench contains two resources: a corpus of 504,587 formally verified C/ACSL programs, and a curated benchmark of 495 tasks designed around function-call composition. The corpus is built by translating verified Rust/Verus seeds into C/ACSL via an LLM-guided semantic mapping loop, in which Frama-C/WP feedback repairs failed candidates. The benchmark is synthesized from verified components by constructing caller functions whose specifications depend on multiple callee contracts. Experiments with six LLMs show that performance drops as the number of function calls increases. The dataset is available at https://huggingface.co/datasets/noBuggie/AcslBench, and the video is available at https://youtu.be/kgvvTajX2Mk.
@inproceedings{paperbot12363,
title = {ACSLBench: A Verified C/ACSL Corpus and Benchmark with Compositional Call Chains for Formal Specification Synthesis},
author = {Junjie Hu and Cheng Wen and Bin Yu and Jialun Cao and Dugang Liu and Weidi Sun and Haokun Li and Shengchao Qin and Cong Tian},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3834628}
}