The SV-COMP competition provides a state-of-the-art platform for evaluating software verification tools on a standardized set of verification tasks. Consequently, verifier development outcomes are influenced by the composition of program benchmarks included in SV-COMP. When expanding this benchmark corpus, it is crucial to consider whether newly added programs cause verifiers to exhibit behavior distinct from that observed on existing benchmarks. Doing so helps mitigate external threats to the validity of the competition's results.
In this paper, we present the application of the ARG-V tool for automatically generating Java verification benchmarks in the SV-COMP format. We demonstrate that, on a newly generated set of 68 realistic benchmarks, all four leading Java verifiers decrease in accuracy and recall compared to their performance on the existing benchmark suite. These findings highlight the potential of ARG-V to enhance the comprehensiveness and realism of verification tool evaluation, while also providing a roadmap for verifier developers aiming to improve their tools' applicability to real-world software.
我们提出了一种新的方法来获得细粒度补丁的Java软件。我们认为一个抽象语法树（AST）表示的Java类编译的Java虚拟机（JVM）的格式，并在AST表示的差异分析，以获得补丁。AST表示定义了一个适当的抽象级别，用于分析差异，产生模块化地与实际源代码更改相关的紧凑补丁。该方法与其他常见的粗粒度方法形成对比，例如简单的二进制差异，这可能很容易导致不成比例的大补丁。我们提出的方法的主要特点，一个原型工具称为ASPA，实现它，并使用ASPA派生补丁的Java 2 SE API的案例研究分析。案例研究结果表明，aspa补丁有一个显着较小的尺寸比补丁由二进制差分工具。
FreshBrew: A Benchmark for Evaluating AI Agents on Java Code Migration
Google（谷歌）；Max Planck Institut für Intelligente Systeme (MPI-IS)（马克斯·普朗克智能系统研究所）；ELLIS Institute, Tübingen（图宾根ELLIS研究所）；Salesforce；Gologic Inc（Gologic公司）
Efficient and Expressive Bytecode-Level Instrumentation for Java Programs
我们提出了一个有效的和富有表现力的工具，在字节码级的Java程序的仪器。BISM（Bytecode-Level Instrumentation for Software Monitoring）是一个轻量级的Java字节码插装工具，它具有一种表达性高的高级控制流感知插装语言。该语言受到面向方面编程范例的启发，将插装模块化为单独的Transformers，封装连接点选择和内联建议。BISM允许捕获从字节码指令到方法执行的连接点，并提供全面的静态和动态上下文信息。它以两种检测模式运行：构建时和加载时。BISM还提供了一种机制来组合Transformers并自动检测它们在基本程序中的冲突。组合中的Transformers可以控制它们的通知和来自基本程序的其他指令的可见性。我们展示了BISM的几个示例应用程序，并使用三个实验证明其有效性：安全场景，金融交易系统和一般运行时验证案例。结果表明，BISM插装引起低的运行时间和内存开销。
