[ldv-project] Version 0.5 of LDV Tools released

[Evgeny Novikov]

The major feature of this release is a control groups based resource 
manager aimed to limit and to count resource consumption of verifiers. 
Linux control groups 
<https://www.kernel.org/doc/Documentation/cgroups/cgroups.txt> allow to 
perform very accurate measurements without any noticeable overhead. 
Other important changes are as follows:

  * Support for automatic verification of modules of the Linux kernel in
    user-defined configurations, including different computer architectures.
  * Addition of the new rule specification Locking and unlocking SDIO
    bus <http://forge.ispras.ru/issues/4360>.
  * Improvements in existing rule specifications: Module get/put
    <http://forge.ispras.ru/issues/3239> and Block requests
    <http://forge.ispras.ru/issues/2706>.
  * Fixing all known segmentation faults
    <http://forge.ispras.ru/issues/4395> in Aspectator.
  * Switch to 2.7.2 <http://forge.ispras.ru/news/282> version of BLAST
    <http://forge.ispras.ru/projects/blast/> verifier.
  * Support of CBMC <http://www.cprover.org/cbmc> verifier as one of LDV
    Tools' back ends.
  * Introducing a standalone error trace visualization tool.

Validation <http://forge.ispras.ru/projects/ldv/wiki/LDV_Validator> of 
LDV Tools 0.5 with different verifiers on 37 known bugs in the Linux 
kernel showed that:

  * BLAST is able to detect 13 of them.
  * CPAchecker is able to detect 11 of them.

In comparison with LDV Tools 0.4 <http://linuxtesting.org/11-10-2013> 6 
known bugs were removed from the validation benchmark since they do not 
fit existing rule specifications, while 5 new known bugs were added to 
the benchmark (3 due to support of user-defined configurations, 1 due to 
addition of the new rule specification and 1 due to determining of an 
appropriate environment model). LDV Tools can detect two of those new 
bugs with help of BLAST verifier.

The source code repository can be browsed by v0.5 
<http://forge.ispras.ru/projects/ldv/repository?utf8=%E2%9C%93&rev=v0.5> 
tag. To get and to install LDV Tools see instructions 
<http://forge.ispras.ru/projects/ldv/wiki/Downloading_and_Building_LDV>.

-- 
Evgeny Novikov
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: novikov at ispras.ru

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20140220/ebb1b31b/attachment.html>