Project

General

Profile

News

Klever 1.0

Added by Evgeny Novikov about 2 months ago

After a long period of development we are happy to release Klever 1.0! This major version is dedicated to verification of Linux loadable kernel modules. Klever 2.0 will allow users to verify various C software.

Klever 1.0 includes all issues scheduled for 0.3 since they take much more time than we expected (we did not release 0.3 at all). Besides, there are many other fixes and improvements. We would like to mention the most valuable ones:

  • Verification results processing, visualization and assessment:
    • More accurate calculation and more pretty visualization of a verification job decision progress.
    • Adding more means for unknown report marks.
    • Improving error traces representation.
  • Updating the CPAchecker verification back-end.
  • Deployment:
    • Developing scripts for local deployment of Klever at Debian 9.
    • Improving deployment within OpenStack clouds.
    • Creating documentation that describes Klever deployment.
  • Support of a command-line interface for Klever Bridge.
  • Continuous integration:
    • Considerable enhancement of Klever tests.
    • Evaluating testing and validation results with preset marks.
    • Automated regression testing with help of Jenkins.
  • Numerous improvements, optimizations and bug fixes that substantially contribute reliability, increase performance and facilitate manual operations. Too many issues to treat them individually.

We thank all the developers and contributors for this great work! Before releasing Klever 2.0 we are going to release at least one minor version 1.1 with many valuable things but without any fundamental changes.

Klever 0.2

Added by Evgeny Novikov 10 months ago

Quite soon after the first release Klever 0.2 is available. Among all new features and bug fixes the most notable ones are the following:
  • Verification results processing, visualization and assessment:
    • Improving calculation and visualization of code coverage for particular verification tasks.
    • Calculation and visualization of code coverage split by correctness rule specifications for verification jobs or sub-jobs as a whole.
    • Switching to new functions for converting and comparing error traces by default as well as removing the outdated ones.
    • Fixes of processing, visualization and comparison of error traces for data races.
  • Verification back-ends:
    • Support for configuring verification back-ends.
    • Updating verification back-ends used by default.
    • Integration of Ultimate Automizer as an alternative verification back-end.
  • Verification tasks generation:
    • Ability to generate verification tasks consisting of several C source files.
    • Parallel generation of verification tasks and processing of verification results.
    • Reusing intermediate results obtained during verification tasks generation.
  • Support for installation and updates within OpenStack clouds.

Klever 0.1

Added by Evgeny Novikov 12 months ago

After more than 2 years of very intensive development we are glad to announce that the first version of Klever was released. Klever 0.1 includes extremely many awesome features to mention all of them explicitly. We just would like to thank all developers and contributors who made this possible.

Starting from Klever 0.1 we will make new releases each several months and, if this will have sense for some users, create stable branches for previous releases to backport fixes of the most critical issues.

GSoC 2016 project was successfully completed

Added by Evgeny Novikov about 2 years ago

Ilja Zakharov has finished works on Google Summer of Code 2016 project "Environment model specifications for more bugs to reveal" for The Linux Foundation.

During the project Ilja has ported all environment model specifications and tests to a new process calculus based environment model generator and implemented new environment model specifications to improve precision of environment models generated during static verification of Linux kernel modules. Moreover, a lot of work has been done to fix bugs in the environment model generator and to implement new features in it. For instance, Ilja has implemented a feature to generate simplified models for huge drivers to get a chance to a verification tool to finish analysis within a reasonable time.

As a result of this work, overall verification false positive rate has been decreased to 75% and a number of missing target bugs has been decreased to 40% from 60% (number of missed confirmed bugs that should be able to detect with our verification system).

Ilja's commits to the environment model generator and specifications sets (commits.ods) have already been reviewed and merged into the master branch of the upstream repository.

Patches to fix errors found with the environment model generator and new specification sets submitted by Ilja's mentor Alexey Khoroshilov:
  1. https://patchwork.kernel.org/patch/8999941/
  2. https://patchwork.kernel.org/patch/9094121/
  3. https://patchwork.kernel.org/patch/9130115/
  4. https://patchwork.kernel.org/patch/9154199/
  5. https://patchwork.kernel.org/patch/9206223/
  6. https://patchwork.kernel.org/patch/9221835/
  7. https://patchwork.kernel.org/patch/9232893/
  8. https://patchwork.kernel.org/patch/9262359/
  9. https://patchwork.kernel.org/patch/9276095/
  10. https://patchwork.kernel.org/patch/9276093/
    (1-4/4)

    Also available in: Atom