Awards
- 13th Competition on Software Verification (SV-COMP'24): CPAchecker (in a similar configuration as in the previous year) wins category FalsificationOverall and a silver medal in category Overall. Additionally, CPAchecker received bronze medals in 3 out of 6 subcategories for verification of C programs. (Complete results)
- 12th Competition on Software Verification (SV-COMP'23): CPAchecker (in a similar configuration as in the previous year) wins bronze medals in the summary categories Overall and FalsificationOverall. (Complete results)
- 11th Competition on Software Verification (SV-COMP'22): CPAchecker (in a similar configuration as in the previous year) wins a silver medal in the summary category Overall, and a gold medal in the category FalsificationOverall for the fifth time in a row. Additionally, CPAchecker received medals in several subcategories for verification of C programs. This is again the highest amount of gold medals and of medals in total among all tools (in total 2x gold, 2x silver, and 1x bronze). (Complete results)
- 10th Competition on Software Verification (SV-COMP'21): CPAchecker (once more configured with a heuristic algorithm selection depending on property and program features) wins the summary categories Overall and FalsificationOverall for the fourth time in a row. The second place in both categories goes to PeSCo, a tool based on CPAchecker that selects an algorithm based on machine learning. Additionally, CPAchecker received medals in several subcategories for verification of C programs. This is again the highest amount of gold medals and of medals in total among all tools (in total 3x gold and 4x silver for CPAchecker, 2x silver and 2x bronze for PeSCo). (Complete results)
- 9th Competition on Software Verification (SV-COMP'20): CPAchecker (again configured with a heuristic algorithm selection depending on property and program features) wins the summary categories Overall and FalsificationOverall for the third time in a row. Additionally, CPAchecker received a medal in each subcategory for verification of C programs. This is the highest amount of gold medals and of medals in total among all tools (in total 3x gold, 3x silver, and 2x bronze). (Complete results)
- 8th Competition on Software Verification (SV-COMP'19): CPAchecker (configured with a heuristic algorithm selection depending on property and program features) wins the summary categories Overall and FalsificationOverall for the second time in a row. The second place in both categories goes to PeSCo, a tool based on CPAchecker that selects an algorithm based on machine learning. In total, CPAchecker received 12 medals (3x gold, 4x silver, and 5x bronze) and at least one in every category for verification of C programs. This is the highest amount of gold medals and of medals in total among all tools. (Complete results)
- 7th Competition on Software Verification (SV-COMP'18): CPAchecker (configured with sequentially combined analyses, similar to last year) wins the summary categories Overall and FalsificationOverall. In total, CPAchecker received 8 medals (4x gold, 2x silver, and 2x bronze). This is the highest amount of gold medals and of medals in total among all tools. (Complete results)
- 6th Competition on Software Verification (SV-COMP'17): CPAchecker participated in this year's competition with several different configurations. CPAchecker (configured with sequentially combined analyses, similar to last year) wins a bronze medal in the summary category Overall. In summary, configurations of CPAchecker reached 1x silver and 2x bronze in different categories. (Complete results)
- 5th Competition on Software Verification (SV-COMP'16): CPAchecker participated in this year's competition with several different configurations. CPAchecker (configured with sequentially combined analyses, similar to last year) wins a silver medal in the summary category Overall. In summary, configurations of CPAchecker reached 3x gold, 4x silver and 2x bronze in different categories. (Complete results)
- 4th Competition on Software Verification (SV-COMP'15): CPAchecker wins the summary category Overall with more than twice the points of the second place. Additionally, it wins the categories ControlFlow and MemorySafety for the second time in a row. In summary, CPAchecker is among the best three verifiers in 8 out of 13 categories, and a tool that is based on CPAchecker (CPArec) is third-best in another category. (Complete results)
-
Copyright (C) Münze Österreich AG - 3rd Competition on Software Verification (SV-COMP'14): CPAchecker wins the 2nd-largest and most traditional category ControlFlow, as well as the categories MemorySafety and Simple (out of 10 categories). CPAchecker and Predator are the only tools that never compute wrong safety proofs for unsafe programs, and CPAchecker has only 12 false alarms, i.e., a total of only 0.4% wrong answers for all 2868 programs. (Complete results)
- 2nd Competition on Software Verification (SV-COMP'13): CPAchecker-based verifiers wins category Overall, and is among the best three verifiers in 9 other categories! (Complete results)
- 1st Competition on Software Verification (SV-COMP'12): CPAchecker-Memo (by University of Paderborn) won the category Overall, and CPAchecker-ABE (by University of Passau) won the category ControlFlowInteger. (Complete results)
Results of CPAchecker in Competitions
Competition on Software Verification
*) including category 'Overall'
Rigorous Examination of Reactive Systems
Competition | Submission | Affiliation | Gold | Silver | Bronze |
---|---|---|---|---|---|
RERS '20 | CPAchecker | LMU Munich | 1 | 1 | |
RERS '19 | CPAchecker | LMU Munich | 2 | 1 | |
RERS '18 | CPAchecker | LMU Munich | 1 | 1 | |
RERS '17 | CPAchecker | LMU Munich | 1 | ||
RERS '16 | CPAchecker | University of Passau | 1 | 1 | |
RERS '14 | CPAchecker | University of Passau | 2 (+2) | 1 | |
RERS '12 | CPAchecker | University of Passau | |||
Total | 8 | 3 | 2 |
Bugs Found with CPAchecker
CPAchecker is used to verify Linux kernel drivers by the Linux Driver Verification project and Klever, and hundreds of bugs in Linux have already been found with CPAchecker and fixed consequently (cf. list of fixes for bugs found with CPAchecker).