Raven: An SMT-Based Concurrency Verifier

This paper presents Raven, a new intermediate verification language and deductive verification tool that provides inbuilt support for concurrency reasoning. Raven's meta-theory is based on the higher-order concurrent separation logic Iris, incorporating core features such as user-definable ghost state and threadmodular reasoning via shared-state invariants. To achieve better accessibility and enable proof automation via SMT solvers, Raven restricts Iris to its first-order fragment. The entailed loss of expressivity is mitigated by a higher-order module system that enables proof modularization and reuse. We provide an overview of the Raven language and describe key aspects of the supported proof automation. We evaluate Raven on a benchmark suite of verification tasks comprising linearizability and memory safety proofs for common concurrent data structures and clients as well as one larger case study. Our evaluation shows that Raven improves over existing proof automation tools for Iris in terms of verification times and usability. Moreover, the tool significantly reduces the proof overhead compared to proofs constructed using the Iris/Rocq proof mode.