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.
What's new?
- AST: new
getName method at RangedVariable class
- AST:
Assignment class fields are renamed
- Bug fixes and general improvements
The release includes the following changes:
- Build system: use Gradle 5.0;
- Documentation: changelog and readme are rewritten into Markdown format;
- Language: support for macro with parameters;
- Language: support for SystemVerilog Assertions;
- Options: `--library-file` option to include function library files;
- Tests: test cases for QUIP and IWLS'2005 benchmarks;
- Tool: bug fixes and general improvements;
- Tool: error diagnostics is improved;
- Tool: migration to Java 11.
The tool can be downloaded from here
The list of resolved issues can be found here