Dear all, The next talk in the IARCS Verification Seminar Series will be given by Vadim Mutilin, a Lead Researcher at ISPRAS and an Associate Professor at MIPT. The talk is scheduled on Tuesday, August 11, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=MXJ1ZTBwcG4wODBta3Y0MWhpcjgwZmFhNDkgdnNzLmlhcmNzQG0&tmsrc=vss.iarcs%40gmail.com> ). The details of the talk can be found on our webpage ( https://fmindia.cmi.ac.in/vss/), and also appended to the body of this email. The Verification Seminar Series, an initiative by the Indian Association for Research in Computing Science (IARCS), is a monthly, online talk-series, broadly in the area of Formal Methods and Programming Languages, with applications in Verification and Synthesis. The aim of this talk-series is to provide a platform for Formal Methods researchers to interact regularly. In addition, we hope that it will make it easier for researchers to explore newer problems/areas and collaborate on them, and for younger researchers to start working in these areas. All are welcome to join. Best regards, Organizers, IARCS Verification Seminar Series ============================================================= Title: Linux Driver Verification: Achievements and Prospects Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting 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. 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.