Ilja Zakharov was one of the greatest contributors to the Klever project. He was the primary developer of such components as Environment Model Generator, Program Fragment Generator, Schedulers and Controller. Besides, he created a lot of environment model specifications for different kinds of target programs and made considerable scientific researches. We appreciate his work very much.
Recently Ilja Zakharov became a Verification Engineer at the Runtime Verification company. There he will be engaged in application of formal methods for smart contracts and tools used for their verification. We wish him good luck and hope that the gained experience will help him at the new position.
The most noticeable work in Klever 3.3 is a new section Development of Environment Model Specifications in the user documentation. Besides, there are following considerable improvements:
- Fixing allocation of memory for arguments of callbacks of several vital Linux device driver types.
- Enhancing environment model specifications for file systems.
- Simplifying development of environment model specifications and fixing some bugs at their processing
- Numerous enhancements of the Klever web UI that simplify several common use cases.
- Updating dependencies and addons that make them more functional and robust.
- Development of unit tests for deployment of Klever within the OpenStack cloud
- Supporting deployment at openSUSE.
- New section Development of Common API Models in the user documentation.
We would like to thank those developers and users who actively contributed to Klever 3.3!
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.
Other important changes are as follows:
- 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.
Version 1.3 of Requality has been released with many scalability and usability improvements.
The new features include:
- Automatic Sequential ID assignment to elements of requirements catalogue
- Support for markup of framed html documents
- Speed up of various operations including:
- project loading
- document import
Also various bugs have been fixed in:
- Import of html documents
- Markup process
- Reports and Report settings
A complete list of changes can be found in changelog.
Klever 3.1 was released!
The new release has the following major changes:
- Improved support for the ARM/ARM64 architecture.
- New parts within the user documentation:
- Fixing existing models and specifications and development of the new ones:
- Support deregistration of pm_ops callbacks.
- Fixing models for vmalloc()/vfree() and friends.
- Developing the model for current.
- Adding the ability to weave in models (#10742).
- Allowing excluding common models (#10716).
- Suggesting working source trees automatically (most likely you will not need to specify them manually for new build bases).
- Showing Klever version in Bridge.
- Updating vital Klever addons and dependencies:
- Support for the new OpenStack cloud at ISP RAS.
Many thanks to all contributors of Klever 3.1!
Уважаемые коллеги!
Redmine обновился до версии 4.1.2.
Просьба сообщать об обнаруженных проблемах.
Let’s start the new year 2021 with new Klever 3.0!
Among a lot of improvements and bug fixes, most significant changes in Klever
3.0 are as follows:
- Support for verification of kernel loadable modules of Linux 5.5.
- Support for verification of Linux kernel loadable modules on the ARM architecture.
- Fixing and developing specifications for verification of Linux kernel loadable modules:
- Fixing specifications for checking usage of clocks in drivers.
- Support for checking usage of the RCU API.
- Developing detailed specifications for USB serial drivers.
- Improving environment models for runtime power management callbacks.
- Using device identifiers from the driver tables.
- Developing models for devm memory allocating functions.
- Fixing framebuffer_alloc/release models.
- Adding models for request/release_firmware(), v4l2_i2c_subdev_init() and i2c_smbus_read_block_data().
- More user-friendly configuration for target program fragments and requirement specifications.
- Development of preset tags for assessing most common false alarms.
- Support for new internal data formats for enhancing and optimizing representation and assessment of verification results.
- Support for cross-references for original program source files and models.
- Update of all variants of the CPAchecker verification back-end.
- Switching to a special version of Frama-C developed within project Deductive Verification Tools for Linux Kernel from outdated and unmaintained CIL. Both tools are used for merging source files and optimizations like removing unused functions.
- Using systemd scripts instead of init.d ones for Klever services.
- Development of Tutorial.
Klever 3.0 is not backward compatible with former versions of Klever, so, you need to remove existing instances if so and deploy Klever from scratch.
As usual many thanks are to everyone who participated in this release of Klever!
Version 1.2 of Requality has been released with many scalability and usability improvements:
- Requirements HTML editor:
- support for preformatted text and indents;
- Properties view:
- search in history properties page and “Switch to…” dialog;
- highlighting of current revision in history tab and revision selection in “Switch to...”;
- speedup of history properties page loading;
- asynchronous operations with attributes.
- Reporting:
- refactoring of reports hierarchy from plain to tree-like with unification of reports naming;
- header with description of revisions in “compare versions“ report;
- Requality interface:
- message box after “Switch to old version“ operation;
- asynchronous loading of requality projects;
- better interface for Checker Rules editor;
- better interface of Requality References.
Experimental features:
- reference versioning with tracking if referenced elements are updated;
- new report for debugging checker rules;
- persisted ”show description on elements” flag.
Also various bugs have been fixed in:
- “compare versions” report;
- git operations — “Switch to ...“, “Reset ...“, etc.
- internal caches;
- attributes panel;
- “mandatory attributes” functionality.
A complete list of changes can be found in changelog.