[FM-India]IARCS Verification Seminar Series -- Talk by Prakash Saivasan on August 6 at 1900 hrs IST

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Prakash Saivasan, an Assistant Professor at the Institute of Mathematical Sciences, Chennai. The talk is scheduled on Tuesday, August 06, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=MWRjc29rN3NyZWk2Mjk3MnFtcjlkazEwcWMgdnNzLmlhcmNzQG0&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, Akash, Deepak, Madhukar, Srivathsan ============================================================= Title: Verifying Programs in Weak Memory Models with Persistency Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: In this talk, we will consider the problem of verifying concurrent programs. In here, we are given a set of programs that communicate through shared memory and a specification, we wish to algorithmically check if the programs violate the specification. The programmers, while writing code usually assume that the memory operations are immediate (referred to as sequential consistency). However, the modern day architectures, to optimise the running time, re-order the memory operations in a non-trivial manner. This leads to various memory models such as TSO, PSO and so on. We will walk through some of these memory models during the talk. The recent intel processor introduced persistency mechanism that allows for the writes to be archived. This can then be used to restart the computation in case of a crash. The main focus of the talk will be how to verify programs when persistency is combined with weak memory. Bio: Prakash Saivasan is an Assistant Professor at the Institute of Mathematical Sciences, Chennai. He obtained his PhD from Chennai Mathematical Institute in 2016 and has done postdocs at T U Braunschweig and T U Kaiserslautern in Germany. His areas of interest are automata theory, logic, concurrency, and formal verification.