Title: Automating Concurrent Separation Logic

Abstract:
Verifying concurrent programs remains a key challenge in formal
verification. Modern concurrent separation logics (CLSs) provide an
extensive toolbox of deductive reasoning techniques that help to
tackle this challenge. However, the expressive power of these logics
comes at the cost of a steep learning curve. Moreover, proofs
typically need to be carried out in interactive theorem provers with
limited support for proof automation, resulting in a high manual proof
effort.
In this talk, I will briefly introduce the key reasoning principles
underlying CLSs and reflect on our recent efforts in building
automated verification tools for such logics. In particular, I will
present Raven, a new intermediate verification language and deductive
verifier for concurrent programs.  Raven’s meta-theory is based on the
higher-order concurrent separation logic Iris, but carefully restricts
the logics expressivity to enable proof automation via SMT solvers. I
will discuss key aspects of Raven’s design, its proof automation
strategies, and report on our experience of using the tool for
verifying linearizability of complex concurrent data structures.