We are happy to announce that Klever 2.0 is released!
Klever 2.0 implements ideas suggested in [1]. In general we added support for verification of software written in the GNU C programming language. First examples of using Klever for software that differs from Linux device drivers are verification of Linux kernel subsystems [2] and BusyBox applets. We are looking forward for more success stories!
Most important changes in Klever
2.0 are the following:
- Klever does not build programs under verification anymore. Instead it takes as input build bases that should be prepared with Clade in advance. This considerably speed ups verification when verifying the same software within different verification jobs. Also, this provides a more natural way to integrate Klever within a standard development life cycle.
- The generator of program fragments (former verification objects) includes abstract means suitable for various software as well as means for particular kinds of programs that allow to avoid considerable efforts for configuring program decomposition.
- The environment models generator consists of a number sub-generators that take specifications in suitable specific formats. This allows to simplify development of such the specifications very much. Besides, we fixed many existing and developed new environment model specifications both for new kinds of interactions between Linux kernel and BusyBox components and for new versions of the Linux kernel.
- The Klever interface provides users with a extremely useful online editor that enables changing configuration and specification files directly within the interface.
As usual many minor improvements and bug fixes were included in Klever 2.0.
Klever 2.0 differs too much from previous versions of Klever. Therefore, we recommend to deploy it from scratch rather than to update existing deployments.
We would like to thank everybody who participated in development, testing and using of Klever!
References
- Novikov E., Zakharov I. (2018) Towards Automated Static Verification of GNU C Programs. In: Petrenko A., Voronkov A. (eds) Perspectives of System Informatics. PSI 2017. Lecture Notes in Computer Science, vol 10742. Springer, Cham.
- Novikov E., Zakharov I. (2018) Verification of Operating System Monolithic Kernels Without Extensions. In: Margaria T., Steffen B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice. ISoLA 2018. Lecture Notes in Computer Science, vol 11247. Springer, Cham.
Klever 1.1 includes quite many high demanded features and fixes of the most annoying bugs:
- Improving coverage calculation and visualization. Now one can easily navigate through covered and uncovered functions.
- Updating CPALockator used for finding data races.
- Proper processing of wall timeouts that is especially important for highly overloaded machines.
- Advanced verification tasks scheduling allows:
- Solving verification tasks faster by means of adaptation of computational resource limits.
- Solving more verification tasks when having free computational resources after ensuring a minimally required quality of service.
- Getting rid of some database caches helps to avoid unpleasant bugs in various statistics.
- Considerable fixing and improving local and OpenStack deployments.
- Numerous minor bug fixes, optimizations and improvements.
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.
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.
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.