Continuous Verification Framework

This framework enables continuous verification of generic software systems. It consists of the following tools:

• Continuous Verifier (CV) Verifies a target software system. To support a specific system, a plugin must define:

  • how to decompose the system (currently supports only C programs);
  • how to construct an environment model;
  • which properties to verify.

  📖 CV Documentation

• Klever Bridge Integrates with the Klever framework to verify Linux kernel modules. 📖 Klever Bridge Documentation

• Benchmark Visualizer Processes and visualizes verification benchmarks from SV-COMP. 📖 Benchmark Visualizer Documentation

• Witness Visualizer Converts SV-COMP witnesses (error traces or proofs) into human-readable format. 📖 Witness Visualizer Documentation

• Multiple Error Analyser (MEA) Filters multiple witnesses to report only unique potential bugs. 📖 MEA Documentation

📊 All verification results can be viewed using the Continuous Verification Visualizer (CVV).

Requirements

Tested on Ubuntu 20.04 and above.

Ubuntu Packages

Install required packages using:

sudo apt update
sudo apt install -y \
  git openjdk-17-jdk python3 python3-dev python3-pip ant lcov cmake

Python Dependencies

Install Python modules with:

pip3 install -r requirements.txt

Installation

Run the following command to install the framework:

make install -j DEPLOY_DIR=<working_directory>

Replace <working_directory> with your preferred deployment path.