News
30-Mar-2017: XIX scientific conference "RusCrypto'2017" took place in Moscow
Submitted by Vadim Mutilin on Wed, 29/03/2017 - 21:00XIX scientific conference "RusCrypto'2017" has taken place in Moscow region on March, 21-24 at "Sunny Park Hotel & SPA" dedicated to information security and privacy.
05-Mar-2017: 4-th International Conference on Tools and Methods of Program Analysis took place in Moscow
Submitted by Vadim Mutilin on Sat, 04/03/2017 - 21:00The 4th Tools & Methods of Program Analysis International Conference (TMPA 2017) organized in cooperation with ACM Sigsoft has taken place in Moscow, Russia. At the conference Pavel Andrianov and Ilja Zakharov gave talks representing Linux Driver Verification project.
30-Nov-2016: Astraver Toolset 1.1 released
Submitted by admin on Wed, 30/11/2016 - 18:28Astraver Toolset 1.1 comes with the following improvements:
C language support
- Initial support for pointer arithmetic involving nested structures e.g. `container_of' macro from the Linux kernel.
In particular, the new implementation allows to prove the validity of the pointer to the outer structure obtained by subtracting the offset of the inner structure from the pointer to that structure.
New approach to support modulo arithmetic operations on values of integral C types in ACSL
27-Sep-2016: 6th Linux Driver Verification Workshop took place in Passau
Submitted by Vadim Mutilin on Mon, 26/09/2016 - 21:006th Linux Driver Verification Workshop was held in Passau, Germany on September 22-23 colocated with 1st International Workshop on CPAchecker.
16-Aug-2016: Analysis of race condition warnings in the Linux kernel
Submitted by admin on Tue, 16/08/2016 - 07:01Pavel 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
Submitted by Vadim Mutilin on Mon, 11/04/2016 - 16:10BLAST 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
Submitted by Vadim Mutilin on Mon, 12/10/2015 - 21:00The 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
Submitted by Vadim Mutilin on Thu, 01/10/2015 - 21:00October 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
Submitted by Vadim Mutilin on Tue, 22/09/2015 - 21:005th 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
Submitted by Vadim Mutilin on Wed, 13/05/2015 - 07:57LDV Tools 0.8 comes with the following improvements:
- Update the CPAchecker verification tool to the new version 1.4 (r14998).
- LDV Tools are now available as Docker images, so you can avoid installation of all dependencies on your machine.
- Improvements in 13 existing rule specifications: