Lilo - A Higher-Order, Relational Concurrent Separation Logic for Liveness

Explore a 15-minute conference presentation introducing a novel higher-order, relational concurrent separation logic framework designed to verify liveness properties in concurrent programs. Learn how this innovative approach addresses the limitations of existing methods like TaDA Live and Fair Operational Semantics by combining refinement proofs, Iris-style invariants, and modular specifications to enable verification of non-terminating programs and concurrent objects with non-local linearization points. Discover the stratified propositions technique inspired by Nola that supports higher-order reasoning without step-indexing, and examine how novel abstractions for liveness reasoning unify various successful techniques from the literature. Study practical applications through case studies including the first termination-guaranteeing modular verification of the elimination stack, with all examples mechanized in Coq and supported by comprehensive artifacts that have been evaluated as reusable with reproduced results.