CPAchecker explained

CPAchecker is a framework and tool for formal software verification,^[1] and program analysis, of C programs. Some of its ideas and concepts, for example lazy abstraction, were inherited from the software model checker BLAST.^[2] CPAchecker is based on the idea of configurable program analysis^[3] which is a concept that allows expression of both model checking and program analysis with one formalism.When executed, CPAchecker performs a reachability analysis, i.e., it checks whether a certain state, which violates a given specification, can potentially be reached.^[4]

One application of CPAchecker is the verification of Linux device drivers.^[5]

Achievements

CPAchecker came first in two categories (Overall and ControlFlowInteger) in the 1st Competition on Software Verification (2012) that was held at TACAS 2012 in Tallinn.^[6]

CPAchecker came first (category Overall) in the 2nd Competition on Software Verification (2013) that was held at TACAS 2013 in Rome.^[7]

Architecture

CPAchecker operates on a control-flow automaton (CFA); before a given C program can be analyzed by the CPA algorithm, it gets transformed into a CFA. A CFA is a directed graph whose edges represent either assumptions or assignments and its nodes represent program locations.

Notes and References

1. Official website of CPAchecker: http://cpachecker.sosy-lab.org
2. Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar. The Software Model Checker BLAST: Applications to Software Engineering. International Journal on Software Tools for Technology Transfer . 2007. 9. 505–525. 10.1007/s10009-007-0044-z. 1662778.
3. Dirk Beyer and Thomas A. Henzinger and Grégory Théoduloz. Configurable Software Verification: Concretizing the Convergence of model Checking and program analysis. Proceedings of the 19th International Conference on Computer Aided Verification. Springer-Verlag, Heidelberg. 2007. 978-3-540-73367-6.
4. Dirk Beyer and M. Erkan Keremoglu. CPAchecker: A Tool for Configurable Software Verification. Proceedings of the 23rd International Conference on Computer Aided Verification. Springer-Verlag, Heidelberg. 2011. 978-3-642-22109-5.
5. Linux Driver Verification: http://linuxtesting.org/project/ldv
6. Dirk Beyer. Competition on Software Verification (SV-COMP). Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and of Analysis Systems. Springer-Verlag, Heidelberg. 2012.
7. Dirk Beyer. Second Competition on Software Verification (Summary of SV-COMP 2013). Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and of Analysis Systems. Springer-Verlag, Heidelberg. 2013.