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]
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.
↑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.