Evaluating Software Verifiers for C, Java, and SV-LIB
摘要
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.