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.
@article{arxiv.1809.03739,
title = {Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP)},
author = {Lucas Cordeiro and Daniel Kroening and Peter Schrammel},
journal= {arXiv preprint arXiv:1809.03739},
year = {2019}
}