Dear all, The next talk in the IARCS Verification Seminar Series will be given by Markus Kuppe, a Principal Research Software Development Engineer in the Research In Software Engineering group at Microsoft Research, Redmond. The talk is scheduled on Tuesday, March 14, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=MzdlMXZ1c2lvNzY1MmtqNzhjMHByNmt1dmggdnNzLmlhcmNzQG0&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: TLA+: The Tools, The Language, and The Application Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: TLA+ is a language for formally specifying and verifying discrete systems, including distributed algorithms. Users describe the system as a state machine, written in a language based on mathematical set theory and temporal logic, which also serves to express safety and liveness properties. TLA+ comes with tools for computer-assisted verification, including two model checkers and an interactive proof system. TLA+ is used in academia and industry, e.g., to verify data consistency in cloud applications. This talk will cover the theory behind TLA+ and how practitioners can write TLA+ specifications with the help of verification tools. Additionally, we will discuss known limitations of the tools and outline current and future research opportunities. Bio: Markus Kuppe is a Principal Research Software Development Engineer in the Research In Software Engineering group at Microsoft Research, Redmond. His focus is on making specification-driven development (with TLA+) more popular among engineers. This includes scaling verification to real-world problems and building tools to combine specification-driven development with established software engineering processes.