CPAchecker
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]
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 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.
References
- ↑ Official website of CPAchecker: http://cpachecker.sosy-lab.org
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ Linux Driver Verification: http://linuxtesting.org/project/ldv
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
- ↑ Lua error in package.lua at line 80: module 'strict' not found.
