News
04-Jul-2018: Klever 1.0 released
Submitted by admin on Wed, 04/07/2018 - 16:31We are happy to announce that a long term work aimed to redesign LDV Tools has been completed by releasing Klever 1.0.
Klever provides a lot of new features including:
28-Jun-2018: Linux Verification Center at Sound Static Analysis for Security Workshop
Submitted by admin on Fri, 29/06/2018 - 19:00
15-Jun-2018: CPA&LDV Workshop 2018 will take place in Moscow
Submitted by Vadim Mutilin on Fri, 15/06/2018 - 11:50The joint 3rd International Workshop on CPAchecker (CPA) and 8th Linux Driver Verification (LDV) Workshop
will take place on September 25-26, 2018 in Moscow, Russia.
23-Apr-2018: CPAchecker-BAM-BnB and CPAchecker-BAM-Slicing at SV-COMP'2018
Submitted by Vadim Mutilin on Sun, 22/04/2018 - 21:00CPAchecker-BAM-BnB and CPAchecker-BAM-Slicing were presented at the 7th International Competition on Software Verification (SV-COMP) held at TACAS 2018 in Thessaloniki, Greece. This year our submission CPAchecker-BAM-BnB has won Gold medal and CPAchecker-BAM-Slicing has won Bronze medal in Software Systems category.
7-Sep-2017: 7th Linux Driver Verification Workshop took place in Paderborn
Submitted by Vadim Mutilin on Thu, 07/09/2017 - 18:387th 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
Submitted by Vadim Mutilin on Mon, 28/08/2017 - 12:23Anton 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:
- searching for bugs related to data races in Linux kernel;
- notifying authors and maintainers about them.
27-Aug-2017: Finding bugs related to the memory errors in Linux kernel
Submitted by Vadim Mutilin on Sun, 27/08/2017 - 05:05Anton 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
Submitted by Vadim Mutilin on Thu, 29/06/2017 - 21:0011th 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
Submitted by Mikhail Mandrykin on Mon, 29/05/2017 - 21:00Our 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
Submitted by Vadim Mutilin on Wed, 26/04/2017 - 21:00CPAchecker-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.
