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.
Contents
One application of CPAchecker is the verification of Linux device drivers.
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.
CPAchecker came first (category Overall) in the 2nd Competition on Software Verification (2013) that was held at TACAS 2013 in Rome.
Architecture
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.