IARCS Verification Seminar Series




Title: Linux Driver Verification: Achievements and Prospects

Speaker: Vadim Mutilin   (bio) (bio)


Vadim Mutilin is a Lead Researcher at ISPRAS and an Associate Professor at MIPT. His research focuses on methods and tools for ensuring software correctness and reliability through static and dynamic verification techniques.

He received his Ph.D. for his work on the verification of Linux device drivers using predicate abstraction. As part of this research, he made significant contributions to the LDV/Klever verification framework and enhanced verification tools such as BLAST and CPAchecker, adapting them for industrial-scale software systems comprising millions of lines of code, including Linux device drivers and real-time operating systems. These tools are currently used at the Center for System Software Security Research.

His research interests include concurrent software verification and the detection of concurrency-related defects. He was one of the key contributors responsible for implementing multithreading support in the ARK TS virtual machine. His current work focuses on scalable techniques for detecting elusive concurrency bugs, including data races, in multithreaded software.

When: Tuesday, 11 August 2026 at 1900 hrs (IST)  

Meeting Details: Zoom link, ID: 891 6409 4870, Passcode: 082194

Abstract:
This talk focuses on the automatic verification of Linux kernel device drivers. I will discuss the unique challenges that device drivers pose for software verification, as well as the characteristics of Linux kernel development that must be taken into account when designing effective verification techniques.

I will present static verification approaches that have helped identify more than 400 real bugs in Linux device drivers. The talk will cover the classes of defects these techniques can detect, their current limitations, and promising directions for future research.