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

Lucas Cordeiro, Daniel Kroening, Peter Schrammel

Research output: Contribution to journalArticlepeer-review

163 Downloads (Pure)

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 in an annual basis, through comparative evaluation of fully-automatic software verifiers for C programs. Building upon this success, we describe here 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 three state-of-the-art Java verification tools, JPF-SE, JayHorn and JBMC.
Original languageEnglish
JournalACM SigSoft Software Engineering Notes
Early online date2 Jan 2019
DOIs
Publication statusPublished - 2019

Fingerprint

Dive into the research topics of 'Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP)'. Together they form a unique fingerprint.

Cite this