Some of its ideas and concepts, for example lazy abstraction, were inherited from the software model checker BLAST.
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] 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.