ARG-V生成的Java验证基准数据集

该数据集由ARG-V工具自动生成，旨在扩充SV-COMP竞赛的Java验证基准库，包含68个具有现实代码特征的基准程序。数据集覆盖可达性安全（ReachSafety）和运行时异常安全（ExceptionProperty）两类验证任务，其中48个属于前者（31真/17假），50个属于后者（39真/11假）。数据来源于RepoReaper数据库中1,261个GitHub仓库，经过程序逻辑筛选和格式转换，平均每个文件41.7行代码，与现有SV-COMP基准规模相当。该数据集通过暴露主流Java验证工具的盲区，推动了形式化验证技术在真实场景中的应用研究。

Automatically generated by the ARG-V tool, this dataset is designed to expand the Java verification benchmark library of the SV-COMP competition, encompassing 68 benchmark programs featuring realistic code characteristics. The dataset covers two categories of verification tasks: ReachSafety and ExceptionProperty. Among them, 48 benchmarks fall into the former category (31 true, 17 false), while 50 belong to the latter (39 true, 11 false). The dataset is sourced from 1,261 GitHub repositories within the RepoReaper database. After undergoing program logic screening and format conversion, each file contains an average of 41.7 lines of code, which is comparable to the scale of existing SV-COMP benchmarks. This dataset advances applied research on formal verification technologies in real-world scenarios by exposing the blind spots of mainstream Java verification tools.

搜集汇总

数据集介绍

构建方式

在软件形式验证领域，基准数据集的代表性直接影响验证工具评估的有效性。ARG-V生成的Java验证基准数据集通过自动化流程构建，其核心机制依托ARG-V工具的三模块架构：下载模块从RepoReaper数据库获取GitHub开源仓库；过滤模块依据用户设定的最小特征阈值（如条件语句、类型表达式）筛选代码文件；转换模块利用Eclipse JDT进行抽象语法树遍历，通过类型表和方法绑定智能移除外部依赖，同时保留核心计算逻辑，并自动生成符合SV-COMP格式的验证脚手架文件和属性定义，最终形成包含68个基准程序的语料库。

特点

该数据集显著区别于传统手工构建的基准，其核心特征体现在真实性与挑战性两个维度。所有基准程序均从真实开源代码中挖掘生成，平均代码行数41.7行，与现有SV-COMP基准规模相当，但程序行为更具现实软件代表性。实验表明，四大主流Java验证工具在该数据集上的准确率与召回率均出现显著下降，未知结果比例高达53%，揭示了验证工具在现实代码场景中存在的盲区。数据集涵盖可达性安全与运行时异常安全两类验证属性，通过最小化人工干预的自动化生成机制，有效避免了基准选择偏差，为验证工具评估提供了更全面的行为覆盖。

使用方法

该数据集主要服务于软件验证工具的性能评估与方法研究。研究人员可通过标准化实验平台BenchExec执行验证任务，配置4GB内存与120秒CPU时间限制，复现论文中的对比实验。数据集支持参数化过滤功能，用户可根据研究目标调整特征阈值（如最小条件语句数、浮点类型使用），定向生成特定行为模式的基准子集。对于验证工具开发者，该数据集可作为识别工具弱点的测试集，通过分析工具在未知结果占比较高的基准上的表现，定位需要改进的算法模块。数据集已集成至SV-COMP Java基准库，可直接用于验证工具的迭代开发与竞赛评估。

背景与挑战

背景概述

在软件形式化验证领域，评估工具性能的标准化基准数据集对于推动技术进步至关重要。ARG-V生成的Java验证基准数据集由内布拉斯加大学林肯分校和博伊西州立大学的研究团队于2026年创建，旨在解决SV-COMP竞赛中Java验证基准代表性不足的问题。该数据集通过自动化工具从真实开源代码中提取并转化生成，核心研究目标是增强验证工具评估的全面性与现实性，从而更准确地反映验证器在实际软件场景中的能力。其生成机制显著提升了基准的多样性和无偏性，对形式化验证方法的发展产生了积极影响。

当前挑战

该数据集致力于应对软件形式化验证中基准测试的现实性挑战，旨在解决现有SV-COMP基准可能无法充分覆盖真实代码复杂行为的问题。构建过程中的主要挑战包括：从海量开源仓库中自动筛选具有验证意义的代码片段，需平衡特征选择标准以避免偏差；移除外部依赖并注入标准化验证库时，需保持程序语义完整性；以及确保生成的基准符合SV-COMP格式规范，同时维持代码逻辑的真实性与可验证性。这些挑战要求工具在自动化处理与语义保真之间实现精细权衡。

常用场景

经典使用场景

在软件形式化验证领域，ARG-V生成的Java验证基准数据集主要用于增强SV-COMP（软件验证竞赛）的基准测试集。该数据集通过自动化工具从真实开源代码中提取并格式化程序，生成了68个具有现实特征的Java基准测试案例，覆盖了可达性安全和运行时异常安全两类验证任务。这些基准程序被设计为包含条件语句、算术表达式等复杂逻辑结构，能够更全面地评估验证工具在多样化代码模式下的性能表现，从而为竞赛提供更丰富和更具挑战性的测试环境。

实际应用

ARG-V数据集在实际应用中，为软件验证工具的开发和评估提供了关键支撑。验证工具开发者可以利用该数据集测试其工具在更接近真实世界代码的场景下的鲁棒性，识别并修复潜在缺陷。例如，数据集中包含涉及浮点数非确定性分支的复杂案例，能够帮助开发者针对数值精度、异常处理等边缘情况进行专项优化。此外，该数据集已集成到SV-COMP竞赛的官方基准库中，为年度竞赛提供了新的测试标准，促进了验证工具在实际工业环境中的适用性提升。

衍生相关工作

该数据集的生成工具ARG-V本身基于早期研究工具PAClab扩展而来，推动了软件验证基准生成领域的技术演进。相关经典工作包括PAClab在方法级程序分析上的探索，以及ARG-V在此基础上增加的跨类交互、多数据类型支持等特性。数据集的应用还衍生出对验证工具如MLB、GDart、JavaRanger和JBMC的深入性能分析，揭示了这些工具在现实基准上的局限性。未来工作方向包括扩展ARG-V以支持C代码转换，以及利用深度学习技术避免生成冗余测试案例，进一步丰富验证基准的生态体系。