Dear all, The next talk in the IARCS Verification Seminar Series will be given by Ilya Sergey, an Associate Professor at the School of Computing of National University of Singapore. The talk is scheduled on Tuesday, July 14, at 1930 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=MmZtZ2RhaXJzcmZvbDl1aTFxbzVnbjUxbWggdnNzLmlhcmNzQG0&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: Multi-Modal Verification of Distributed Systems in Lean Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: In this talk, I will present Veil, a framework for automated and interactive verification of transition systems, aimed specifically at conducting machine-assisted proofs about concurrent and distributed algorithms. Veil is implemented on top of the Lean proof assistant. It allows one to describe a transition system and its specification in a simple imperative language, verifying it using both dynamic and symbolic execution techniques. Veil allows one to check the desired safety properties in the style of TLA+ using explicit-state model-checking. For symbolic deductive reasoning, Veil produces verification conditions in first-order logic, to be discharged automatically via a range of SMT solvers. In case automated verification fails or if the system's description requires statements in a higher-order logic, Veil provides an interactive verification mode, by virtue of being embedded in a general-purpose proof assistant. Veil's automated verification performance is acceptable for practical verification tasks, while it also allows for seamless automated/interactive verification of system specifications beyond the reach of existing automated provers. Bio: Ilya Sergey is an Associate Professor at the School of Computing of National University of Singapore, where he leads the Verified Systems Engineering lab. He received his PhD from KU Leuven. Before joining NUS, he was a postdoc at IMDEA Software Institute and a faculty at University College London. Ilya's research spans programming language design, software verification, and distributed systems. He is a Program Committee Co-Chair for OOPSLA'27, was General Chair for ICFP 2025, and organised the ICFP Programming Contest in 2019. He is the recipient of several POPL/PLDI distinguished paper awards, the 2019 Dahl-Nygaard Junior Prize, and research awards from Google, Meta, and Amazon.