CASP

CASP数据集是一个针对C代码形式化验证的评估数据集，包含506对用ANSI/ISO C规范语言（ACSL）编写的形式化规范和相应的C代码。该数据集由AI Sweden、Scania和KTH皇家理工学院的研究人员创建，旨在填补现有数据集在规模和多样性方面的不足，并支持对大型语言模型（LLMs）在代码生成和验证方面的性能进行基准测试。数据集内容丰富，涵盖了从大型开源数据集中提取的C代码及其形式化规范，每个规范-实现对都经过形式化验证。CASP数据集为研究人员提供了一个宝贵的资源，用于训练和评估LLMs在从代码生成规范和反之亦然方面的能力，从而推动软件验证工具的发展，促进更可靠软件系统的创建。The CASP dataset is an evaluation dataset for formal verification of C code. It contains 506 pairs of formal specifications written in the ANSI/ISO C Specification Language (ACSL) and their corresponding C code. This dataset was created by researchers from AI Sweden, Scania, and the Royal Institute of Technology (KTH), aiming to fill the gaps in scale and diversity of existing datasets and support benchmarking the performance of Large Language Models (LLMs) on code generation and verification tasks. The dataset is rich in content, covering C code and their formal specifications extracted from large-scale open-source datasets, with each specification-implementation pair having undergone formal verification. The CASP dataset provides researchers with a valuable resource for training and evaluating LLMs' capabilities in generating specifications from code and vice versa, thereby advancing the development of software verification tools and facilitating the creation of more reliable software systems.

原始信息汇总

CASP_dataset 数据集概述

数据集基本信息

• 名称: CASP_dataset
• 来源: Hugging Face 数据集平台
• 存储位置: https://huggingface.co/datasets/nicher92/CASP_dataset

数据规模

• 总样本数: 506 条
• 总数据量: 1,702,402 字节
• 下载大小: 444,955 字节
• 数据拆分: 仅包含训练集（train）

数据特征结构

数据集包含以下10个字段：

字段名称	数据类型	描述
file_name	string	文件名
verified_c_file_content	string	已验证的C文件内容
dependency_acls	string	依赖ACLs
function_implementation	string	函数实现
verified	bool	验证状态
total_goals	int64	总目标数
verified_goals	int64	已验证目标数
error_cause	string	错误原因
c_code_snippet	string	C代码片段
acsl_snippet	string	ACSL片段

数据配置

• 配置名称: default
• 数据文件路径: data/train-*

搜集汇总

数据集介绍

构建方式

在形式化验证领域，CASP数据集通过多阶段筛选流程从The Stack v1和v2代码库中系统性地提取C代码与ACSL形式化规约对。首先采用正则表达式识别包含ACSL注释的C文件，随后通过Frama-C框架的WP和RTE插件进行形式化验证，并利用大语言模型对未通过验证的文件进行迭代修复。最终通过人工检查确保每对规约-代码组合的正确性，形成506个经过严格验证的最小完整单元。

特点

该数据集的核心特征在于其严格的形式化验证保障和结构设计。所有代码-规约对均通过Frama-C工具链验证，确保功能正确性与运行时安全性；采用最小完整依赖设计，仅保留标准库引用以支持独立验证；数据来源具有高度多样性，涵盖不同编程风格和算法实现。其双向评估结构支持从代码生成规约和从规约生成代码的双重研究任务，为形式化方法与大语言模型结合提供了标准化基准。

使用方法

数据集以函数-规约对的形式组织，可直接用于大语言模型的训练与评估。研究者可通过加载标准化JSON格式数据，分别提取ACSL规约和C实现进行生成任务测试。验证阶段需配置Frama-C环境，调用WP插件配合Z3、Alt-Ergo等SMT求解器进行形式化证明。数据集支持零样本评估和微调实验，特别适用于代码生成模型的可靠性验证、规约推断算法的性能测试以及形式化方法工具的基准评估。

背景与挑战

背景概述

CASP数据集由瑞典AI Sweden研究院联合斯堪尼亚汽车公司与皇家理工学院于2025年共同创建，旨在解决形式化验证领域缺乏大规模标注数据集的瓶颈问题。该数据集聚焦于C语言程序与ACSL形式化规范的配对验证，通过从The Stack v1和v2代码库中提取506对经过Frama-C工具链严格验证的代码-规范样本，为大型语言模型在代码生成与形式化验证结合的交叉研究提供了基准测试基础。其创新性体现在首次实现了从海量开源代码中自动化筛选、修复并验证形式化规范的工作流程，推动了高可靠性软件系统的开发范式转型。

当前挑战

在领域问题层面，CASP需解决形式化验证中代码与规范双向生成的核心挑战：一是如何确保LLM生成的代码严格满足ACSL规范的内存安全性与功能正确性；二是如何验证自动生成的规范与代码实现间的逻辑一致性。在构建过程中面临三重技术挑战：首先是从数千万C文件中精准识别含ACSL注释的样本，需设计多级正则过滤与语义验证流程；其次是修复非验证文件时需平衡LLM自动化修复与人工校验的精度，仅成功修正19.9%的异常文件；最后是依赖项剥离的复杂性，必须剔除非标准库依赖以构建自包含验证单元，同时保持原始代码语义完整性。

常用场景

经典使用场景

在形式化验证领域，CASP数据集为研究者提供了标准化的评估基准，特别适用于测试大型语言模型在生成符合ACSL规范的C代码方面的能力。该数据集通过精心筛选的506对代码-规范组合，确保了每对都经过Frama-C工具的严格验证，为自动化代码生成与形式化验证的结合研究奠定了坚实基础。

解决学术问题

CASP数据集有效解决了形式化验证研究中缺乏大规模、高质量基准数据的问题。它通过提供经过验证的代码-规范对，支持对LLM生成代码的正确性进行系统评估，推动了自动化软件验证方法的发展，并为安全关键系统的可靠性研究提供了重要资源。

衍生相关工作

CASP数据集已经催生了多项重要研究，例如基于LLM的规范自动修复技术和双向代码-规范生成框架。这些工作利用CASP的高质量验证对，探索了形式化规范与代码之间的自动转换，为构建更可靠的软件系统提供了新的方法论支持。