4 Apr
2025
4 Apr
'25
5:42 p.m.
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.