News

24-Jun-2014: The LDV team gave a talk at the 9th Ershov Informatics Conference

LDV team member Ilja Zakharov gave a talk “Modeling Environment for Static Verification of Linux Kernel Modules” at the 9th Ershov Informatics Conference. The talk presented results of joint research with Alexey Khoroshilov, Vadim Mutilin and Evgeny Novikov dedicated to modeling environment of Linux kernel modules for the purpose of their static verification using modern software model checking tools.

Ilja Zakharov at PSI'2014

29-Apr-2014: Linux Driver Verification is presented at Dagstuhl Seminar

Linux Driver Verification Team members, Alexey Khoroshilov and Vadim Mutilin, took part in the Dagstuhl Seminar on Evaluating Software Verification Systems: Benchmarks and Competitions at April 21–25, 2014. The seminar was organized by Dirk Beyer (Universität Passau), Marieke Huisman (University of Twente), Vladimir Klebanov (Karlsruher Institut für Technologie) and Rosemary Monahan (NUI Maynooth).

17-Apr-2014: BLAST 2.7.2 at SV-COMP'2014 and LDV experiments

BLAST 2.7.2 was presented at the 3rd International Competition on Software Verification held at TACAS 2014 in Grenoble, France. This year BLAST won the gold medal in the DeviceDrivers64 category.

BLAST 2.7.2 at SV-COMP'2014

14-Apr-2014: 4th Linux Driver Verification Workshop took place in Passau

4th Linux Driver Verification Workshop was held in Passau, Germany on April 2-4. The workshop was arranged by prof. Alexander Petrenko (Linux Verification Center, ISPRAS, Moscow, Russia) and prof. Dirk Beyer (University of Passau, Germany).

10-Mar-2014: Linux Verification Center at Embedded World 2014

Vadim Mutilin and Evgeny Novikov have taken part in Embedded World 2014 in cooperation with Open Source Automation Development Lab (OSADL) on February 25-27, Nuremberg, Germany.

20-Feb-2014: Version 0.5 of LDV Tools released

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 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.

11-Oct-2013: Version 0.4 of LDV Tools released

After more then 2 years of active development we are happy to announce that we released LDV Tools 0.4. This version includes a lot of improvements and many bug fixes. In total it consists of about 900 commits that were made just in the LDV Tools repository not including submodules. The most significant changes are:

23-Jun-2013: 3rd Linux Driver Verification Workshop took place in Moscow

3rd Linux Driver Verification workshop was held in Moscow, Russia at June, 19-21. The workshop was arranged by prof. Alexander Petrenko (Linux Verification Center, ISPRAS, Moscow, Russia) and prof. Dirk Beyer (University of Passau, Germany).

12-May-2013: LDV project - the first 100 bugs in Linux kernel fixed

The first 100 bugs found by the Linux Driver Verification project have been fixed in the Linux kernel. 86 patches developed by members of the LDV team have found their way to the mainline kernel.

15-Mar-2013: BLAST 2.7.1 at SV-COMP'2013 and LDV experiments

BLAST 2.7.1 was presented at the 2nd Software Verification Competition 2013 that took place at TACAS'13. This year BLAST won a Bronze in the DeviceDrivers64 category. The second place is taken by CPAchecker which is already integrated into Linux Driver Verification toolset. The winner of DeviceDrivers64 is a new tool named UFO.