Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP)
This work addresses the need for standardized and reproducible benchmarking in the software verification community, specifically for Java tools, but it is incremental as it builds on an existing framework.
The paper tackled the problem of benchmarking Java verification tools by adapting the SV-COMP ecosystem, originally for C programs, to include Java tools, and reported experimental results from a benchmarking run on tools like JPF, SPF, JayHorn, and JBMC.
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.