Klever

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.