Leaf: Modularity for Temporary Sharing in Separation Logic

Explore a 19-minute conference talk from OOPSLA2 2023 that introduces Leaf, a novel library in the Iris separation logic for handling temporarily shared state in concurrent verification. Discover how Leaf addresses the challenges of verifying new sharing strategies and manipulating shared state agnostically through its innovative guarding operator. Learn about the modular case study demonstrating Leaf's effectiveness in verifying a reader-writer lock supporting shared state and a hash table built on top of it. Gain insights into the advancements in concurrent separation logic, verification techniques, and the handling of fractional and counting permissions. Access the accompanying article and supplementary archive for a deeper understanding of this research presented by experts from Carnegie Mellon University and VMware Research.

[OOPSLA23] Leaf: Modularity for Temporary Sharing in Separation Logic