Continuous Verification Framework

This framework aims at applying continuous verification to generic software systems. The framework consist of the following tools:

• Continuous Verifier (CV) verifies a given software systems. In order to support generic software system, a specific plugin is required, which shows

  • how to decompose a system (currently, only C language is supported);
  • how to create an environment for the system;
  • what properties should be verified in the system.

  CV documentation.

• Klever Bridge allows to verify Linux kernel modules with help of Klever framework. Klever Bridge documentation.

• Benchmark Visualizer allows to process and visualise verification benchmarks from SV-COMP. Benchmark Visualizer documentation.

• Witness Visualizer converts generic witnesses (potential bug or proof) from SV-COMP tools into user-friendly format. Witness Visualizer documentation.

• Multiple Error Analyser (MEA) filters several witnesses in order to present only those, which corresponds to unique potential bugs. Witness Visualizer documentation.

All produced verification results can be visualised with help of Continuous Verification Visualizer.

Requirements

The framework works with Ubuntu 18 and above. All requirements can be installed with command:

sudo apt install git openjdk-11-jdk python3 python3-dev ant lcov cmake libmpc-dev lib32z1 libxslt-dev libpq-dev python3-pip

Additional python modules:

sudo pip3 install requests ujson graphviz ply pytest atomicwrites pathlib2 more-itertools pluggy py attrs setuptools six django clade==3.6 psycopg2 pyyaml pycparser sympy

Installation

The framework is installed with the following command:

make install -j DEPLOY_DIR=<working dir>