Overview

Klever is a static verification framework that aims at automated checking of programs developed in the GNU C programming language against a variety of correctness rules using tools implementing such methods of thorough static analysis as Bounded Model Checking and Counterexample-Guided Abstraction Refinement.

The current version of Klever allows to find memory safety issues, e.g. buffer over-reads/writes and null pointer dereferences, data races and incorrect usages of the most popular Linux kernel API as well as to prove formal correctness under certain assumptions for Linux kernel loadable modules. We have implemented specifications for modeling interrupts, timers and interfaces of kernel subsystems including USB, PCI, SCSI, SERIAL, NET, file systems, etc. Klever 1.0 will complete support of automated static verification for other CNU C software.

As static verification back-ends Klever supports CPAchecker and Ultimate Automizer. Moreover, one can integrate other tools participated in the competition on software verification.

For starting static verification and for comprehensive analysis of results Klever provides a multiuser web graphical interface. It shows both details, e.g. error traces that contain all statements and possible values of variables and function arguments from a program start to a found error, and statistics like the total number of bugs and false alarms. Experts can create marks associating automatically with all similar results.

If you have any questions, feel free to send an email to .

Issue tracking

View all issues | Calendar