|
CPAchecker is a framework and tool for formal software verification,〔Official website of CPAchecker: http://cpachecker.sosy-lab.org〕 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. One application of CPAchecker is the verification of Linux device drivers.〔Linux Driver Verification: http://linuxtesting.org/project/ldv〕 ==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. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「CPAchecker」の詳細全文を読む スポンサード リンク
|