Dear all, The next talk in the IARCS Verification Seminar Series will be given by Nikhil Swamy, a researcher at Microsoft Research in Redmond. The talk is scheduled on Tuesday, April 8, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=Mm5wcm80ZWZwanU0Ym5hdWVucTVhcGF0NXEgdnNzLmlhcmNzQG0&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: Pulse: Proof-oriented Programming with Concurrent Separation Logic in F* Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: F* is a dependently typed programming language. It has been used to develop more than a million lines of verified code and proofs, for artifacts ranging from cryptographic libraries to networking components. Some of this verified software runs in widely used production systems, ranging from the Windows kernel to the Python standard library. However, most of this corpus of verified code is purely sequential. Pulse is a new extension of F* enabling programming and proving imperative programs with shared-memory concurrency. Proofs in Pulse are conducted in a new program logic called PulseCore, a concurrent separation logic with state-of-the-art features, including higher-order ghost state and impredicative invariants, backed by a foundational semantics developed within F* itself. Programs are verified in Pulse using a custom checker with a combination of tactics and SMT solving. Once proven, programs in Pulse can be extracted to OCaml, C, or Rust, depending on the libraries and features used. Pulse is being used in a number of new projects, including in the development of verified firmware, in new libraries for secure data formatting, and for verified CPU/GPU programs. I will provide some background on F* and concurrent separation logic, and then introduce Pulse by way of examples and a tool demonstration. Bio: Nikhil Swamy is a researcher at Microsoft Research in Redmond, working in the Research in Software Engineering (RiSE) group. He is interested in type systems, program logics, functional programming, program verification and interactive theorem proving, and also in the use of these techniques to build provably secure programs, including web applications, web browsers, crypto protocol implementations, and low-level systems code.