News

7-Sep-2017: 7th Linux Driver Verification Workshop took place in Paderborn

7th Linux Driver Verification Workshop was held in Paderborn, Germany on September 4-5 colocated with 2nd International Workshop on CPAchecker.

28-Aug-2017: Finding bugs related to the data races in Linux kernel

Anton Volkov has finished his Google Summer of Code project "Finding bugs related to the data races in Linux kernel" for The Linux Foundation. The goals of the GSoC project were:

  1. searching for bugs related to data races in Linux kernel;
  2. notifying authors and maintainers about them.

27-Aug-2017: Finding bugs related to the memory errors in Linux kernel

Anton Vasilyev has finished Google Summer of Code 2017 project "Finding bugs related to the memory errors in Linux kernel" for The Linux Foundation.
Memory errors at the kernel of operation system are a kind of bugs that lead to grave consequences but are hard to detect. Debug and disclose of kernel memory corruptions often requires specially compiled kernel.

30-Jun-2017: A.P. Ershov Informatics Conference took place in Moscow

11th A.P. Ershov Informatics Conference (the PSI Conference Series) has taken place in Moscow, Russia. At the conference Evgeny Novikov and Ilja Zakharov, who represent the Linux Driver Verification project, gave a talk dedicated to features and problems of application of existing static verification tools to arbitrary GNU C programs.

30-May-2017: AstraVer plugin was presented at Frama-C & SPARK Day 2017

Our experience in deductive verification of Linux kernel components using Frama-C with AstraVer plugin, including our combined model for bounded integers, was presented at Frama-C & SPARK Day 2017 held on May, 30th at Université Paris-Diderot, Paris, France.

27-Apr-2017: CPAchecker-BAM-BnB and BLAST 2.7.3 at SV-COMP'2017

CPAchecker-BAM-BnB and BLAST 2.7.3 were presented at the 6th International Competition on Software Verification (SV-COMP) held at TACAS 2017 in Uppsala, Sweden.

30-Mar-2017: XIX scientific conference "RusCrypto'2017" took place in Moscow

XIX 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

The 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

Astraver 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

6th Linux Driver Verification Workshop was held in Passau, Germany on September 22-23 colocated with 1st International Workshop on CPAchecker.