Abstraction Refinement for Model Checking: Program Slicing + CEGAR

Thomas Lemberger

Abstract

Program slicing and counterexample-guided abstraction (CEGAR) are two established approaches to program abstraction in software verification. Both are similar in their concept, with one main difference: Program slicing works on the syntactic level, while CEGAR works on the semantic level. Because of the complexity of software and the complex behavior of the two algorithms, the difference in the capabilities of the two is not clear. To contribute towards understanding this technique, we design a program slicing technique that is based on CEGAR and that performs program slicing on dynamically computed slicing criteria. We implement this technique in the widely used software verification framework CPAchecker, and extend it to be combine-able with any other, existing abstraction refinement based on CEGAR. As a proof of concept, we combine it with the CEGAR-based symbolic execution engine in CPAchecker. In a next step, we extend the existing state-of-the-art, LLVM-based program slicer Symbiotic to use CPAchecker as a verification back-end. To combine theses two tools, we also implement a new LLVM front-end in CPAchecker that enables CPAchecker to analyze LLVM programs. As a last step, to get a better understanding of the behavior of our analyses, we implement an abstract graph visualization technique, called pixel trees. Pixel trees allow users to grasp the structure of the programstate space that got explored by an analysis run, even for graphs that are too large to comprehend in a detail view. We perform a thorough evaluation of all presented techniques. Through this, we are able to show that program slicing and CEGAR are two complementing technologies, and that their combination can have a significant impact on verification performance.

Experimental Data

A comparison table of our results can be found here (csv).

Configuration HTML CSV Logfiles Witnesses Pixel Trees
SymEx HTML CSV Logfiles Witnesses Pixel Trees
SymEx with Slicing HTML CSV Logfiles Witnesses Pixel Trees
SymEx with CEGAR HTML CSV Logfiles Witnesses Pixel Trees
SymEx with Slicing + CEGAR HTML CSV Logfiles Witnesses Pixel Trees
Symbiotic HTML CSV Logfiles
Symb+ HTML CSV Logfiles
Symb+ with CEGAR HTML CSV Logfiles

Pixel Trees

In the following, we show two examples for the pixel trees of SymEx with slicing, with CEGAR and with a combination of both, to show the different behavior of these three approaches.

Task SymEx with Slicing SymEx with CEGAR SymEx with Slicing + CEGAR
trex_01_true-unreach-call_true-termination.i SVG SVG SVG
linux-3.8-rc1-32_7a-drivers--net--dsa--mv88e6xxx_drv.ko-ldv_main2_true-unreach-call.cil.out.c SVG timeout SVG
Problem01_label44-false-unreach SVG SVG SVG

Execution

We provide an artifact that contains the experimental data and all tools necessary to repeat our results.

Requirements

We tested this artifact on the SoSy-Lab Virtual Machine.

If you don't use it, we assume that you have:

We recommend:

This will be enough for running the small examples below. For repeating our experiments under proper settings, the following is required, in addition:

Have fun!

Example Task

We use the running example from our Master's thesis as an example task to try the different symbolic execution techniques on.

To run CPAchecker with the different configurations, run from this artifact's root directory the following commands on the command line. You can stop execution of CPAchecker by pressing Ctrl+C .

Each run will produce various output in directory output, e.g., the ARG as graph (ARG.dot), the pixel tree of the ARG (ARG.svg), and a verification report (Report.html).

Benchmarks

To repeat our experiments with CPAchecker, change to directory cpachecker and run the following commands in the command line.

The results will be in directory results of the current folder.

To repeat our experiments with symbiotic, change into folder symbiotic-spin2018 and run on the command line:

    benchexec ../benchmark_defs/symbiotic.xml

To repeat our experiments with symbiotic and CPAchecker as a backend, change into folder symbiotic-cpachecker and run on the command line the corresponding commands:

The results will be in directory results of the current folder.

Results Table

To create a large table with all your results, put all created data (*.xml.bz2 files and *.logfiles.zip files) into a new folder raw_data and run on the command line

    table-generator -x table_defs/cpachecker.xml

This will create files table_defs/cpachecker.table.html and table_defs/cpachecker.table.csv.