[FM-India] IARCS Verification Seminar Series -- Talk by Aseem Rastogi on May 10 at 1900 hrs IST

VSS IARCS vss.iarcs at gmail.com
Tue May 3 11:32:50 IST 2022


Dear all,

The next talk in the IARCS Verification Seminar Series will be given by
Aseem Rastogi, a Principal Researcher at Microsoft Research India. The talk
is scheduled on Tuesday, May 10, at 1900 hrs IST (add to Google calendar
<https://calendar.google.com/event?action=TEMPLATE&tmeid=MnM4bDJoMmN1N2QwMmhkN2MzdWVqMXNwY2kgdnNzLmlhcmNzQG0&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: Proof-oriented Programming in F*

Meeting Link:
https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09
(Meeting ID: 891 6409 4870, Passcode: 082194)

Abstract: F* is a proof-oriented programming language that has been used to
develop, and deploy, critical software components backed with mathematical
proofs of correctness and security. Deployments of programs written and
proven in F* include Microsoft Windows Hyper-V, Microsoft Azure, Firefox,
Linux, mbedTLS, and several other production systems. In this talk, I will
begin with an overview of F* and its applications. I will then talk about
our recent work on Steel, a language for programming and proving concurrent
programs embedded in F*. Steel is based on a higher-order Concurrent
Separation Logic, also derived in F* using a denotation of computations in
the effectful semantics of non-deterministically interleaved atomic
actions. With Steel we have programmed several verified programs and
libraries, including spinlocks, protocol-indexed channel, and various
sequential and concurrent data-structures.

Bio: Aseem Rastogi is a Principal Researcher at Microsoft Research India.
His work spans the areas of language design, type systems, program
verification, and software security. More specifically, his interest lies
in developing formal techniques for writing provably correct and secure
software. He is one of the core designers and developers of F*, a language
for program verification.


More information about the FMIndia mailing list