Title: Raven: a concurrency-aware intermediate verification language

Speaker: Ekanshdeep Gupta    (bio) (bio)

Ekanshdeep Gupta is a sixth-year PhD student at NYU graduating in August 2026. His research interests include automated reasoning and program verification tools, particularly using SMT-based automation and combining them with interactive theorem provers. Ekanshdeep is currently on the job market starting September 2026 for industry R&D positions combining programming languages, formal methods and automated reasoning.

When: Tuesday, 09 June 2026 at 1900 hrs (IST)       

Abstract:
We present Raven, a concurrency-aware intermediate verification language (IVL) designed to prove linearizability of concurrent algorithms and data structures. Most front-end verification tools such as Dafny, Verus, and Prusti are based on IVLs like Boogie and Viper, which do not support concurrency. This means that front-end developers must model concurrency semantics on top of the IVL—a complex and error-prone task that must be performed from scratch for each new front-end. By providing concurrency support directly within the IVL, Raven aims to offer a compelling new foundation for developing custom front-ends that enable sophisticated concurrency reasoning.

Raven is based on the Iris Separation Logic Framework, which has demonstrated impressive success in academic circles due to its expressiveness and generality. However, being mechanized in Rocq, Iris has a high barrier to entry and provides little automation. By bringing strong SMT-based automation to Iris, Raven enables linearizability verification at scale and makes the power of Iris accessible to a broader audience. We have implemented and verified a library of concurrent data structures with Raven, including the Michael-Scott queue, Treiber stack, ticket lock, and B+ trees.