[FM-India]IARCS Verification Seminar Series -- Talk by Kartik Nagar on June 4 at 1900 hrs IST

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Kartik Nagar, an Assistant Professor at Department of CSE, IIT Madras. The talk is scheduled on Tuesday, June 04, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=MWlzcXUyN29pN2psMGpyb2w3ZGdpM202cnQgdnNzLmlhcmNzQG0&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: Specifying and Verifying Correctness of Mergeable Replicated Data Types Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: Modern decentralized applications often use multiple replicas/copies of data, each of which can be independently operated, to minimize data access latency, provide fault tolerance and improve scalability. Mergeable Replicated Data Types (MRDTs) have emerged as a systematic approach to the problem of ensuring that replicas remain eventually consistent despite concurrent conflicting updates. MRDTs draw inspiration from the Git version control system, where each update creates a new version and any two versions can be merged explicitly through a user-defined merge function. The full flexibility offered by MRDTs in terms of creating and merging arbitrary versions severely complicates the design and development of correct MRDT implementations. In this talk, I will present two orthogonal approaches for specification and verification of MRDTs: a highly expressive, axiomatic event-based specification approach supported by a semi-automated verification procedure, and a more intuitive (but restrictive) linearizability based specification approach supported by fully automated verification. Bio: Kartik Nagar is an Assistant Professor at Department of CSE, IIT Madras. He completed his PhD from IISc Bangalore, after which he was a postdoc at Purdue University. His research interests are in Automated Formal Verification, Program Analysis and Programming Languages, with emphasis on developing practical verification techniques for concurrent and distributed systems.