Dear all, The next talk in the IARCS Verification Seminar Series will be given by Shaz Qadeer, an ACM Fellow, currently employed as a software engineer in the Core Infrastructure department at Meta. The talk is scheduled on Tuesday, July 11, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=MHF2OTJoMmlkcW1vdjYycWc5cmRzcGhmaTMgdnNzLmlhcmNzQG0&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: Verification of Concurrent Programs with Civl Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: The Civl verifier <https://civl-verifier.github.io/> introduces layered refinement, a new approach to the construction of verified concurrent programs and their proofs. This approach simplifies and scales (human and automated) reasoning by enabling a concurrent program to be represented and manipulated at multiple layers of abstraction. These abstraction layers are chained together via simple program transformations; each transformation is justified by a collection of automatically-checked verification conditions. Civl proofs are maintainable and reusable, specifically eliminating the need to write complex invariants on the low-level encoding of the concurrent program as a flat transition system. Civl has been used to construct verified low-level implementations of complex systems such as a concurrent garbage collector, a consensus protocol, and shared-memory data structures. Bio: Shaz Qadeer is an ACM Fellow. His research focuses on practical tools for the construction of verified concurrent and distributed systems. He is currently employed as a software engineer in the Core Infrastructure department at Meta.