Title: Pulse: Proof-oriented Programming with Concurrent Separation Logic in F*

Speaker: Nikhil Swamy    (bio) (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.

When: Tuesday, 08 April 2025 at 1900 hrs (IST)       

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.