Multithreaded shared memory programs appear in many applications such as operating systems, web servers, mobile applications etc. Verification of such programs has been of increasing concern since the early 2000s when clock speeds stabilised, with the focus shifting to architectures with multiple cores. From a theoretical perspective, any problem is undecidable already for programs with just two recursive threads since one can then simulate a Turing machine. Hence we focus on restricting the problems to runs of the program which are context-bounded i.e. where every thread can be active at most K many times for some fixed number K. This restriction has been effective at finding bugs since from a practical standpoint most bugs occur already with a low number of context switches. We resolve long standing open problems related to the complexity of safety and liveness verification of multithreaded programs in the presence of context bounding. This talk is aimed at giving a high level overview of these results.
Bio: Ramanathan Thinniyam is currently a postdoc at the Max Planck Institute for Software Systems in the Rigorous Software Engineering group. He obtained his BTech in Mechanical Engineering in IIT Madras, MSc in Theoretical Computer Science(TCS) at CMI and PhD in TCS at IMSc.
He has been working on theoretical aspects of verification of multithreaded programs and has published in conferences such as ICALP, POPL and TACAS.
