CPAchecker is a framework and tool for formal software verification, and program analysis, of C programs. Some of its ideas and concepts, for example lazy abstraction, were inherited from the software model checker BLAST. CPAchecker is based on the idea of configurable program analysis  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. 
CPAchecker operates on a control-flow automata (CFA); before a given C program can be analysed 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.
- Official website of CPAchecker: http://cpachecker.sosy-lab.org
- Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar (2007). "The Software Model Checker BLAST: Applications to Software Engineering" (PDF). International Journal on Software Tools for Technology Transfer (STTT) 9: 505–525.
- Dirk Beyer and Thomas A. Henzinger and Grégory Théoduloz (2007). "Configurable Software Verification: Concretizing the Convergence of model Checking and program analysis" (PDF). Proceedings of the 19th International Conference on Computer Aided Verification. Springer-Verlag, Heidelberg. ISBN 978-3-540-73367-6.
- Dirk Beyer and M. Erkan Keremoglu (2011). "CPAchecker: A Tool for Configurable Software Verification" (PDF). Proceedings of the 23rd International Conference on Computer Aided Verification. Springer-Verlag, Heidelberg. ISBN 978-3-642-22109-5.
- Linux Driver Verification: http://linuxtesting.org/project/ldv
- Dirk Beyer (2012). "Competition on Software Verification (SV-COMP)" (PDF). Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and of Analysis Systems. Springer-Verlag, Heidelberg.
- Dirk Beyer (2013). "Second Competition on Software Verification (Summary of SV-COMP 2013)" (PDF). Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and of Analysis Systems. Springer-Verlag, Heidelberg.