CPAchecker

CPAchecker is a tool for configurable software verification which means expressing different program analysis and model checking approaches in one single formalism. The main algorithm is configurable to perform a reachability analysis on arbitrary combinations of existing configurable program analysis (CPA). One application of CPAchecker is the verification of Linux device drivers.

CPA provides a conceptual basis for expressing different verification approaches in the same formal setting. The CPA formalism provides an interface for the definition of program analyses, which includes the abstract domain, the post operator, the merge operator, and the stop operator. Consequently, the corresponding tool implementation CPAchecker provides an implementation framework that allows the seamless integration of program analyses that are expressed in the CPA framework. The comparison of different approaches in the same experimental setting becomes easy and the experimental results will be more meaningful.

Architecture

CPAchecker

The above picture is the overview of CPAchecker’s architecture. The central data structure is a set of control-flow automata (CFA), which consist of control-flow locations and control-flow edges. A location represents a program-counter value, and an edge represents a program operation, which is either an assume operation, an assignment block, a function call, or a function return. Before a program analysis starts, the input program is transformed into a syntax tree, and further into CFAs. The framework provides interfaces to SMT solvers and interpolation procedures, such that the CPA operators can be written in a concise and convenient way. From the picture, we know that they use MathSAT as an SMT solver, and CSIsat and MathSAT as interpolation procedures. They also use JavaBDD as a BDD package, and provide an interface to an Octagon Library as well. The CPA Algorithm is the center of this project and the detailed design is shown as follows.

CPAchecker

The CPA algorithm (shown at the top in the above figure) takes as input a set of control-flow automata (CFA) representing the program, and a CPA, which is in most cases a Composite CPA. The interfaces correspond one-to-one to the formal framework. The elements in the gray box (top right) represent the abstract interfaces of the CPA and the CPA operations. The two gray boxes at the bottom of the figure show two implementations of the interface CPA, one is a Composite CPA that can combine several other CPAs, and the other is a Leaf CPA.

Build and Test

Owing to the long development history, this project is very prefect which means you could use its binary directly, build from the source and even use their jar-ball in Java applications. To experience it, I will build it from the source and use it in the command-line.

We need to install “jdk”, “ant”, “svn” and “subversion” before we build it. Then enter the root directory and run “ant”. Wait a moment and this is the result.

To test this project, we need to write a C/C++ code without “#include ”. I choose a simple one (QuickSort) shown in the attachment.

The result contains a log file, a statistics file and a report which is in “html” format.



本文链接: http://home.meng.uno/articles/c5d9877c/ 欢迎转载!

© 2018.02.08 - 2020.06.02 Mengmeng Kuang  保留所有权利!

UV : | PV :

:D 获取中...

Creative Commons License