Context-bounded Verification of Multithreaded Shared Memory Programs (Delivered in English)
- LecturerProf. Ramanathan Thinniyam Srinivasan (Uppsala University, Sweden)
Host: Yu-Fang Chen - Time2025-02-21 (Fri.) 10:00 ~ 12:00
- LocationAuditorium107 at IIS new Building
Abstract
Multithreaded shared memory programs are ubiquitous and can be found in web servers, operating systems, mobile applications etc. Verifying correctness of such programs is therefore important, yet difficult because of the high degree of concurrency in such programs. In fact, all problems of interest become undecidable for a program with just two recursive threads. Context-bounded analysis (CBA) is a successful practically applied underapproximation technique in this scenario. The inventors of CBA were given the prestigious CAV 2023 award. In this talk, we will an overview of the work on computational complexity of safety, liveness and other problems of interest in the verification of such programs under CBA.
BIO
Speaker is currently assistant professor at uppsala university, prior to which he did his postdoc at Max Planck Institute for SoftWare Systems (mpi-sws) with Rupak Majumdar and Georg Zetzsche. His postdoc work on Context-bounded analysis was published in top venues such as ICALP, POPL, TACAS . This work was recognised by a Distinguished Paper Award at POPL 2021 and EAPLS Best Paper Award 2021, as well as an invited paper at ICALP 2023.