Awards

Results of CPAchecker in Competitions

Competition on Software Verification

Competition Submission Affiliation Gold Silver Bronze
SV-COMP '22 CPA-BAM-SMGISP RAS1
CPAcheckerLMU Munich23*1
Graves-CPAUniversity of Virgina1
PeSCoUniversity of Paderborn11
SV-COMP '21 CPA-BAM-BnBISP RAS
CPALockatorISP RAS
CPAcheckerLMU Munich3*4
PeSCoUniversity of Paderborn2*2
SV-COMP '20 CPA-BAM-BnBISP RAS1
CPALockatorISP RAS
CPA-SeqLMU Munich3*32
PeSCoUniversity of Paderborn2*
SV-COMP '19 CPA-BAM-BnBISP RAS1
CPA-LockatorISP RAS
CPA-SeqLMU Munich2*24
PeSCoUniversity of Paderborn2*1
SV-COMP '18 CPA-BAM-BnBISP RAS1
CPA-BAM-SlicingISP RAS1
CPA-SeqLMU Munich3*21
SV-COMP '17 CPA-BAM-BnBISP RAS
CPA-kIndUniversity of Passau
CPA-SeqUniversity of Passau12*
SV-COMP '16 CPA-kIndUniversity of Passau12
CPA-RefSelUniversity of Passau1
CPA-SeqUniversity of Passau23*
LPIVERIMAG
UL-CSeqUniversities of Stellenbosch / Southampton
SV-COMP '15 CPAcheckerUniversity of Passau3*32
CPArecAcademia Sinica1
UL-CSeqUniversities of Stellenbosch / Southampton
SV-COMP '14 CPAcheckerUniversity of Passau31*1
CPAlienBrno University of Technology
SV-COMP '13 CPAchecker-ExplicitUniversity of Passau4*
CPAchecker-SeqComUniversity of Passau1*6
SV-COMP '12 CPAchecker-ABEUniversity of Passau11*2
CPAchecker-MemoUniversity of Paderborn1*21
Total273634

*) including category 'Overall'

Rigorous Examination of Reactive Systems

Competition Submission Affiliation Gold Silver Bronze
RERS '20 CPAcheckerLMU Munich11
RERS '19 CPAcheckerLMU Munich21
RERS '18 CPAcheckerLMU Munich11
RERS '17 CPAcheckerLMU Munich1
RERS '16 CPAcheckerUniversity of Passau11
RERS '14 CPAcheckerUniversity of Passau2 (+2)1
RERS '12 CPAcheckerUniversity of Passau
Total411

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).