Evaluating Software Verifiers for C, Java, and SV-LIB

View at publisher
Authors: Dirk Beyer, Jan Strejček
Cited by: 6
References: 153

Abstract

Abstract The Competition on Software Verification (SV-COMP) regularly evaluates software verifiers and witness validators processing programs in C and Java. SV-COMP 2026 evaluated 61 verifiers and 16 validators for C programs and 11 verifiers and 3 validators for Java programs. Out of these, 43 verifiers and 13 validators participated with an active support of teams led by 44 different representatives from 12 countries. The verification track of the competition was executed on a benchmark set of 36 402 verification tasks with C programs and 6 different specifications  and 1 731 verification tasks with Java programs and 2 different specifications. The validation track analyzed 229 118 witnesses generated in the verification track for C programs and also 135 handcrafted witnesses. On top of that, SV-COMP 2026 considered also 254 verification tasks in the recently introduced format SV-LIB and evaluated 3 verifiers and 1 validator for this format. Moreover, there was also a demo category sponsored by Huawei, consisting of selected verification tasks with concurrent C programs. To keep our growing competition sustainable and up to date, we made several changes in its processes and settings.

Fields of Study & Subjects

Software Testing and Debugging Techniques Software Engineering Research Logic programming and type systems

Publication details

Journal / source
Lecture notes in computer science
Publisher
Springer Nature Switzerland
Pages
461–502
Publication date
1 January 2026
Language
EN