Context-bounded Verification of Multithreaded Shared Memory Programs (以英文演講)
- 講者Ramanathan Thinniyam Srinivasan 教授 (瑞典烏普薩拉大學)
邀請人：陳郁方 - 時間2025-02-21 (Fri.) 10:00 ~ 12:00
- 地點資訊所新館107演講廳
摘要
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.