News
23-Aug-2021: Finding bugs related to memory errors in Linux Kernel
Submitted by Vadim Mutilin on Mon, 23/08/2021 - 16:31Nadezda Lutovinova has finished the GSoC 2021 project “Finding bugs related to memory errors in Linux Kernel and improving environment model specifications for static verification”. Her project was related to finding memory errors in Linux drivers code. During the work Nadezda has used Klever - a software verification framework that is created for automated checking of programs developed in the C programming language. It was used to analyze the Linux kernel version 5.12-rc3 code.
20-Aug-2021: Analysis & Fixing of Race Condition Warnings in the Linux Kernel
Submitted by Vadim Mutilin on Fri, 20/08/2021 - 07:22Saubhik Mukherjee has finished the GSoC 2021 Project "LSB: Analysis & Fixing of Race Condition Warnings in the Linux Kernel" for The Linux Foundation. The task is to catch bugs due to race conditions in Linux kernel 5.4 device drivers. A software verification framework called Klever automates the verification against a concurrency safety requirement specification. Using the Klever web interface, the generated error traces are analyzed and classified as false warnings or real bugs.
31-Aug-2020: Development of environment model specifications for static verification of Linux Kernel
Submitted by Vadim Mutilin on Mon, 31/08/2020 - 16:47Nadezda Lutovinova has finished the GSoC 2020 Project "Development of environment model specifications for static verification of Linux Kernel" for The Linux Foundation.
28-Aug-2020: Analysis and fixing of race condition warnings in the Linux kernel
Submitted by Vadim Mutilin on Fri, 28/08/2020 - 10:32Madhuparna Bhowmik has finished the GSoC 2020 Project “Analysis and fixing of race condition warnings in the Linux kernel” for The Linux Foundation. The project involved using Klever interface for finding the race condition related bugs in the v4.18 of the Linux Kernel, and most of them were still present in the latest kernel release which is v5.9. Out of the 301 traces analyzed around 44 of them were either Actual Bugs or Benign bugs. This gives a true positive rate of 14.6%.
10-Dec-2019: The start of a project on formal modeling and verification of software
Submitted by Vadim Mutilin on Mon, 09/12/2019 - 21:00
4-Oct-2019: CPA&LDV Workshop took place in Frauenchiemsee
Submitted by Vadim Mutilin on Fri, 04/10/2019 - 10:03CPA&LDV Workshop was held in Frauenchiemsee, Germany on October 1-2, 2019.
6-Apr-2019: CPAchecker-BAM-BnB and CPALockator at SV-COMP'2019
Submitted by Vadim Mutilin on Sun, 07/04/2019 - 15:10CPAchecker-BAM-BnB and CPALockator were presented at the 8th International Competition on Software Verification (SV-COMP) held at TACAS 2019 in Prague, Czechia. This year our submission CPAchecker-BAM-BnB has won Gold medal in Software Systems category and CPALockator participated in Concurrency Safety category.
1-Feb-2019: The book about modeling and verification of access control policies in operating systems is published
Submitted by Vadim Mutilin on Thu, 31/01/2019 - 21:00We are happy to announce availability of "Modeling and verification of access control policies in operating systems" book issued by publishing house "Goryachaya Liniya - Telekom". The book is written by P.N. Devyanin (RusBiTech) and members of Linux Verification Center team within AstraVer project.
27-Sep-2018: CPA&LDV Workshop took place in Moscow
Submitted by Vadim Mutilin on Thu, 27/09/2018 - 13:44CPA&LDV Workshop was held in Moscow, Russia on September 25-26.
13-Aug-2018: Improve environment model for memory safety verification of the Linux kernel and find bugs related to the memory errors in Linux kernel
Submitted by Vadim Mutilin on Mon, 13/08/2018 - 10:30Anton Vasilyev has finished Google Summer of Code 2018 project "Improve environment model for memory safety verification of the Linux kernel and find bugs related to the memory errors in Linux kernel" for The Linux Foundation.