Dear all, The next talk in the IARCS Verification Seminar Series will be given by Sumanth Prabhu, a scientist in the Foundations of Computing group at TCS Research. The talk is scheduled on Tuesday, May 07, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=NzZsODVrdDVwNDRqaml2YTMwbGtqZTNmM3UgdnNzLmlhcmNzQG0&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: Weakest Precondition Inference for Linear Array Programs Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: The problem of precondition inference is to find a set of initial states from which all terminating executions of a given program reach states that satisfy a given postcondition. The weakest precondition refers to the largest such set of initial states. The weakest precondition is helpful in many practical problems around software development, verification, and testing. Hence, its automatic inference is an important problem and has received considerable attention. However, existing techniques find it challenging to handle programs with arrays. In this talk, I will present our technique to find quantified weakest preconditions for programs with arrays. Our technique is effective on a class of programs called linear array programs. We prove that linear array programs' weakest precondition computation is undecidable. Nevertheless, such programs often appear in practice. Hence, many array works target them but for verification, not precondition inference. We propose a precondition inference technique in the Infer-Check-Weaken framework. It first infers a precondition along with adequate inductive invariants. A maximality check follows to see whether the precondition is the weakest. If not, the precondition is weakened. In this framework, we present novel methods for each module. We experimentally show that our technique is significantly better than the state-of-the-art over a set of existing linear array programs. Bio: Sumanth Prabhu works as a scientist in the Foundations of Computing group at TCS Research. He did his Ph.D. from the Indian Institute of Science, Bangalore, where he was advised by Deepak D'Souza. His current research focuses on formal verification and automated synthesis using constrained horn clauses.