6-Apr-2019: CPAchecker-BAM-BnB and CPALockator at SV-COMP'2019

CPAchecker-BAM-BnB and CPALockator were presented at the 8th International Competition on Software Verification (SV-COMP) held at TACAS 2019 in Prague, Czechia. This year our submission CPAchecker-BAM-BnB has won Gold medal in Software Systems category and CPALockator participated in Concurrency Safety category.

Results of SV-COMP 2019 are available here: https://sv-comp.sosy-lab.org/2019/results/results-verified. The tables highlight the winners of the different categories.

CPAchecker-BAM-BnB is based on a joint work with CPAchecker team. BAM stands for Block Abstraction Memoization which enables reuse of verification results during the analysis. BnB is a modification of memory model in predicate analysis (see our paper).

CPALockator implements a thread-modular approach for verification of multithreaded software (see our poster). Abstraction from thread interaction allows to increase the speed of the analysis. As a trade off, the level of precision is decreased, which may lead to false alarms. In contrast with other model checkers CPALockator successfully solves big benchmarks based on Linux device drivers. Some of the tasks are solved only by CPALockator. However, the current implementation has technical limitations, for example, the tool supports only synchronization primitives based on locks, thus loosing the scores on artificial benchmarks implementing lock-free algorithms. Nevertheless, CPALockator does not produce incorrect true results (does not miss bugs), that confirms the soundness of the approach.

We thank CPAchecker community for their contributions to the platform we are basing on.