Demo Categories in SV-COMP 2026
SV-COMP 2026 has three demo meta categories in the verification track and three demo meta categories in validation track. The results will be published below when the results are available.
Demo Category C.Huawai-Concurrency-Challenges in the Verification Track
We are happy to announce that this year Huawei is sponsoring a demo meta category containing some concurrency challenges contributed by Huawei and some benchmarks selected from C.Concurrency (see Huawei-Concurrency-Challenges.set). The meta category C.Huawai-Concurrency-Challenges consists of four base categories, one for each of the the properties no-data-race, no-overflow, unreach-call, and valid-memsafety. The top 3 actively participating tools with a positive score and without any Huawei employees in the team will receive the following prizes:
- Prize: 3000 EUR
- Prize: 1500 EUR
- Prize: 500 EUR
In the base categories of this meta category, receiving points is not conditioned by witness confirmation. Note that producing witnesses (where they are supported) is still mandatory: witness validation is applied and the results are shown, but they do not affect the score.
Please note that Huawei also sponsors travel support for participants of SV-COMP (not restricted to the teams participating in this demo category).
Demo Category SV-LIB.Overall in the Verification Track
The community has developed SV-LIB, a new intermediate format for verification tasks (imperative programs and their specification). The new language will induce new base categories.
Demo Category C.WallTime in the Verification Track
Coming soon.
Demo Categories C.Concurrency and C.Termination in the Validation Track of Correctness Witnesses Version 2
The community has introduced a new witness format 2.1 that supports correctness witnesses for multi-threaded programs (for properties no-overflow and unreach-call) and for termination. Validation of those witnesses is performed already in SV-COMP 2026 optionally, it will be mandatory from SV-COMP 2027 onwards.
Demo Category Java.valid-assert.Main in the Validation Track of Correctness Witnesses Version 1
The witness format 1.0 supports the property valid-assert (called assert_java until SV-COMP 2025). In the past, we have overlooked that there exists at least one validator able to handle such correctness witnesses of this property. SV-COMP 2026 opens a demo category for validation of such witnesses.