News

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:

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