Dear all, The next talk in the IARCS Verification Seminar Series will be given by Subodh Sharma, a faculty member in the Department of Computer Science and Engineering at IIT Delhi. The talk is scheduled on Tuesday, September 6, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/event?action=TEMPLATE&tmeid=NWNpZWM5bTR2YzV1c20yb3Q1b2ljMWQ2MXQgdnNzLmlhcmNzQG0&tmsrc=vss.iarcs%40gmail.com> ). The details of the talk can be found on the 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, Deepak, Madhukar, Rahul, Srivathsan ============================================================= Title: Exploiting partial orders and symmetries in efficient analysis of message-passing concurrency Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: The message passing paradigm is the lingua franca for developing large distributed-memory programs, such as high-performance scientific computing and event-driven web applications. Message-passing applications are often found to be using communication nondeterminism (used primarily to obtain efficiency by masking network latencies) and symmetric communication among processes (which keeps programming simple). Under communication nondeterminism, a process can post (possibly asynchronous) receive calls that can potentially match any of the messages sent to the process. Under symmetric communication, a process's communication structure may be partly or completely symmetric with the communication structure of other processes. Interestingly, communication nondeterminism is one of the important sources of analysis complexity and detecting symmetries is, in general, hard. This talk will present practical techniques to efficiently analyse message passing programs by (i) exploiting partial order among the communication dependencies and (ii) detecting symmetries in process-communication. The work in this talk has been published in TOPLAS 2017, FM 2018, ICST 2021, and ASE 2022. Bio: Subodh Sharma is a faculty member in the Department of Computer Science and Engineering at IIT Delhi. His research interests lie in the area of software engineering and formal methods, particularly in ensuring the reliability of parallel software via static and dynamic program analyses, model checking, and PL solutions, and employing HPC towards the creation of scalable verification technology. Lately, his research investigations have also spanned the areas of systems security, data privacy, and Blockchain.