Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP)

TL;DR

This paper discusses how the SV-COMP benchmarking ecosystem, originally for C verification tools, is adapted for Java verification tools, providing a standardized, reproducible evaluation framework and experimental results.

Contribution

It introduces a detailed methodology for benchmarking Java verification tools within the SV-COMP framework, including rules, integration procedures, and experimental evaluation.

Findings

Benchmarking framework successfully adapted for Java tools

Experimental results compare JPF, SPF, JayHorn, JBMC

Framework enhances reproducibility and standardization in Java verification

Abstract

Empirical evaluation of verification tools by benchmarking is a common method in software verification research. The Competition on Software Verification (SV-COMP) aims at standardization and reproducibility of benchmarking within the software verification community on an annual basis, through comparative evaluation of fully automatic software verifiers for C programs. Building upon this success, here we describe how to re-use the ecosystem developed around SV-COMP for benchmarking Java verification tools. We provide a detailed description of the rules for benchmark verification tasks, the integration of new tools into SV-COMP's benchmarking framework and also give experimental results of a benchmarking run on state-of-the-art Java verification tools, JPF, SPF, JayHorn and JBMC.