Top Qs
Timeline
Chat
Perspective
CPAchecker
Software testing tool written in Java From Wikipedia, the free encyclopedia
Remove ads
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]
Remove ads
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.
References
External links
Wikiwand - on
Seamless Wikipedia browsing. On steroids.
Remove ads