Dear all, The next talk in the IARCS Verification Seminar Series will be given by Ramneet Singh, an AI Researcher at Proximal, working on synthetic RL environment generation for post-training of LLMs. The talk is scheduled on Friday, September 11, at 1500 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=M2VlN3A2ZDg1bGo2YnZxdXAxc2tlNHNucXQgdnNzLmlhcmNzQG0&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: INTERLEAVE: A Faster Symbolic Algorithm for Maximal End Component Decomposition Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: The talk presents a novel symbolic algorithm for the Maximal End Component (MEC) decomposition of a Markov Decision Process (MDP). The key idea behind our algorithm INTERLEAVE is to interleave the computation of Strongly Connected Components (SCCs) with eager elimination of redundant state-action pairs, rather than performing these computations sequentially as done by existing state-of-the-art algorithms. Even though our approach has the same complexity as prior works, an empirical evaluation of INTERLEAVE on the standardized Quantitative Verification Benchmark Set demonstrates that it solves 19 more benchmarks (out of 379) than the closest previous algorithm. On the 149 benchmarks that prior approaches can solve, we demonstrate a 3.81x average speedup in runtime. Bio: Ramneet is currently an AI Researcher at Proximal, working on synthetic RL environment generation for post-training of LLMs. Prior to this, he was a Research Fellow at Microsoft Research India, working on AI agents for large-scale software engineering tasks. He acquired a background in formal methods at IIT Delhi and Georgia Tech, where the work being presented was done as part of his Master's Thesis. He loves thinking about how to formally specify system behaviour and believes it has become even more important today.