<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=ISO-8859-1">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>The major feature of this release is a control groups based
resource manager aimed to limit and to count resource consumption
of verifiers. Linux <a
href="https://www.kernel.org/doc/Documentation/cgroups/cgroups.txt">control
groups</a> allow to perform very accurate measurements without
any noticeable overhead. Other important changes are as follows:</p>
<ul>
<li>Support for automatic verification of modules of the Linux
kernel in user-defined configurations, including different
computer architectures.</li>
<li>Addition of the new rule specification <a
href="http://forge.ispras.ru/issues/4360">Locking and
unlocking SDIO bus</a>.</li>
<li>Improvements in existing rule specifications: <a
href="http://forge.ispras.ru/issues/3239">Module get/put</a>
and <a href="http://forge.ispras.ru/issues/2706">Block requests</a>.</li>
<li>Fixing all known <a href="http://forge.ispras.ru/issues/4395">segmentation
faults</a> in Aspectator.</li>
<li>Switch to <a href="http://forge.ispras.ru/news/282">2.7.2</a>
version of <a href="http://forge.ispras.ru/projects/blast/">BLAST</a>
verifier.</li>
<li>Support of <a href="http://www.cprover.org/cbmc">CBMC</a>
verifier as one of LDV Tools' back ends.</li>
<li>Introducing a standalone error trace visualization tool.</li>
</ul>
<p><a href="http://forge.ispras.ru/projects/ldv/wiki/LDV_Validator">Validation</a>
of LDV Tools 0.5 with different verifiers on 37 known bugs in the
Linux kernel showed that:</p>
<ul>
<li>BLAST is able to detect 13 of them.</li>
<li>CPAchecker is able to detect 11 of them.</li>
</ul>
<p>In comparison with <a href="http://linuxtesting.org/11-10-2013">LDV
Tools 0.4</a> 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.</p>
<p>The source code repository can be browsed by <a
href="http://forge.ispras.ru/projects/ldv/repository?utf8=%E2%9C%93&rev=v0.5">v0.5</a>
tag. To get and to install LDV Tools see <a
href="http://forge.ispras.ru/projects/ldv/wiki/Downloading_and_Building_LDV">instructions</a>.</p>
<pre class="moz-signature" cols="72">--
Evgeny Novikov
Linux Verification Center, ISPRAS
web: <a class="moz-txt-link-freetext" href="http://linuxtesting.org">http://linuxtesting.org</a>
e-mail: <a class="moz-txt-link-abbreviated" href="mailto:novikov@ispras.ru">novikov@ispras.ru</a></pre>
</body>
</html>