News

16-Aug-2016: Analysis of race condition warnings in the Linux kernel

Pavel Andrianov has finished Google Summer of Code 2016 project "Analysis of race condition warnings in the Linux kernel" for The Linux Foundation.

Race conditions are a kind of bugs that are hard to detect — they may manifest itself only on rare schedules, and they are hard to fix — they often require rethinking and careful selection of synchronization mechanism.

11-Apr-2016: BLAST 2.7.3 at SV-COMP'2016

BLAST 2.7.3 was presented at the 5th International Competition on Software Verification (SV-COMP) held at TACAS 2016 in Eindhoven, Netherlands. This year BLAST has won the bronze medal in the DeviceDriversLinux64 category.

13-Oct-2015: LDV project - the 200 bugs in Linux kernel fixed

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

02-Oct-2015: 10th Anniversary of the Linux Verification Center

October 22, Thursday, at 18.00, the panel section "ISPRAS Linux Verfication Center: First Ten Years" will take place at Digital October Center as a part of Central and Eastern European Software Engineering Conference.

23-Sep-2015: 5th Linux Driver Verification Workshop took place in Moscow

5th Linux Driver Verification Workshop dedicated to the 10th anniversary of the Linux Verification Center of ISPRAS was held in Moscow, Russia on September 15-18. The workshop was arranged by prof. Alexander Petrenko (Linux Verification Center, ISPRAS, Moscow, Russia) and prof. Dirk Beyer (University of Passau, Germany).

13-May-2015: Version 0.8 of LDV Tools released

LDV Tools 0.8 comes with the following improvements:

20-Apr-2015: BLAST 2.7.3 at SV-COMP'2015

BLAST 2.7.3 was presented at the 4rd International Competition on Software Verification (SV-COMP) held at TACAS 2015 in London, United Kingdom. This year BLAST has won the gold medal in the DeviceDrivers64 category.

18-Feb-2015: The first public release of Astraver Toolset

We are happy to announce the first public release of Astraver Toolset 1.0 that is built on top of the 'Frama-C + Jessie + Why3 IDE' deductive verification toolchain. The toolchain was adapted, so it can be used to specify and prove properties of Linux kernel code. The most of our modifications go to the Jessie plugin, while the Frama-C front-end and the Why3 platform have got just minor fixes or improvements.

16-Jan-2015: Version 0.7 of LDV Tools released

LDV Tools 0.7 comes with quite a lot improvements and bug fixes:

27-Aug-2014: Version 0.6 of LDV Tools released

LDV Tools 0.6 includes the following most important changes: