Klever

The major improvement of Klever 3.2 is a new environment model generator that supports automated splitting of complex environment models into sets of smaller ones. This is extremely helpful at verification of large programs and program fragments when verification tools often can not provide definite answers within specified time limits.

• Substantially fixed and enhanced representation of violation witnesses (error traces) and code coverage reports as well as navigation through them.
• New environment models for the Linux kernel (the bitmap API and several functions working with strings).
• New validation set on the base of faults found by Klever and fixed in the Linux kernel.
• Supporting more reliable and efficient deployment of Klever within the OpenStack cloud.
• New section Analysis of Code Coverage Reports in the Klever tutorial.

In addition, Klever 3.2 includes numerous minor improvements and bug fixes.

This release would not be possible without intensive work of developers and testers. Also, we always look forward and welcome a feedback from users.