Generically Automating Separation Logic by Functors, Homomorphisms, and Modules

This conference talk from POPL 2025 presents a novel approach to automating Separation Logic (SL) using abstract algebras. Explore how researchers from Nanyang Technological University, Singapore Institute of Technology, Griffith University, and Peking University developed a theory that specifies SL predicates through functors, homomorphisms, and modules over rings. Learn about their generic SL automation algorithm capable of reasoning about data structures characterized by these algebras, along with algorithms for automatically instantiating algebraic models to real data structures. The presentation demonstrates how this compositional approach reuses algebraic models of component structures while preserving data abstractions. Discover case studies on formalized imperative semantics showing automatic instantiation of algebraic models for complex data structures, with experimental results indicating comparable performance to state-of-the-art systems using specifically crafted reasoning rules. All theories, proofs, and the verification framework are formalized in Isabelle/HOL, with artifacts available and evaluated as reusable.