Dear all, The next talk in the IARCS Verification Seminar Series will be given by Ekanshdeep Gupta, a sixth-year PhD student at NYU graduating in August 2026. The talk is scheduled on Tuesday, June 09, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=NDlsNjlxbTZjZGpoaGtkNWJmN2M0NzhkaTggdnNzLmlhcmNzQG0&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, Organizers, IARCS Verification Seminar Series ============================================================= Title: Raven: a concurrency-aware intermediate verification language Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: We present Raven, a concurrency-aware intermediate verification language (IVL) designed to prove linearizability of concurrent algorithms and data structures. Most front-end verification tools such as Dafny, Verus, and Prusti are based on IVLs like Boogie and Viper, which do not support concurrency. This means that front-end developers must model concurrency semantics on top of the IVL—a complex and error-prone task that must be performed from scratch for each new front-end. By providing concurrency support directly within the IVL, Raven aims to offer a compelling new foundation for developing custom front-ends that enable sophisticated concurrency reasoning. Raven is based on the Iris Separation Logic Framework, which has demonstrated impressive success in academic circles due to its expressiveness and generality. However, being mechanized in Rocq, Iris has a high barrier to entry and provides little automation. By bringing strong SMT-based automation to Iris, Raven enables linearizability verification at scale and makes the power of Iris accessible to a broader audience. We have implemented and verified a library of concurrent data structures with Raven, including the Michael-Scott queue, Treiber stack, ticket lock, and B+ trees. Bio: Ekanshdeep Gupta is a sixth-year PhD student at NYU graduating in August 2026. His research interests include automated reasoning and program verification tools, particularly using SMT-based automation and combining them with interactive theorem provers. Ekanshdeep is currently on the job market starting September 2026 for industry R&D positions combining programming languages, formal methods and automated reasoning.