Английская Википедия:CPAchecker

Материал из Онлайн справочника
Перейти к навигацииПерейти к поиску

Шаблон:Short description 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 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

Шаблон:Reflist

External links