BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/1196
DTSTAMP:20230914T125954Z
SUMMARY:Context-Bounded Verification of Multithreaded Shared Memory Program
 s
DESCRIPTION:Speaker: Ramanathan Thinniyam (Max Planck Institute for Softwar
 e Systems)\n\nAbstract: \nMultithreaded shared memory programs appear in m
 any applications such as operating systems\, web servers\, mobile applicat
 ions etc. Verification of such programs has been of increasing concern sin
 ce 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 threa
 ds since one can then simulate a Turing machine. Hence we focus on restric
 ting the problems to runs of the program which are context-bounded i.e. wh
 ere 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 practi
 cal standpoint most bugs occur already with a low number of context switch
 es. We resolve long standing open problems related to the complexity of sa
 fety and liveness verification of multithreaded programs in the presence o
 f context bounding. This talk is aimed at giving a high level overview of 
 these results.\nBio: Ramanathan Thinniyam is currently a postdoc at the Ma
 x Planck Institute for Software Systems in the Rigorous Software Engineeri
 ng 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.\nH
 e has been working on theoretical aspects of verification of multithreaded
  programs and has published in conferences such as ICALP\, POPL and TACAS.
 \n
URL:https://www.tcs.tifr.res.in/web/events/1196
DTSTART;TZID=Asia/Kolkata:20220405T160000
DTEND;TZID=Asia/Kolkata:20220405T170000
LOCATION:Via Zoom
END:VEVENT
END:VCALENDAR