Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore the formal framework for reasoning about translational separation logic verifiers in this 21-minute conference talk from POPL 2025. Presented by researchers from ETH Zurich and the University of British Columbia, the video introduces a generic core Intermediate Verification Language (IVL) that captures the essence of different separation logics. Learn how this framework addresses the challenges of proving soundness in translational verifiers by connecting input programs and verification logic to IVL semantics. The presentation details how angelic non-determinism enables different proof search algorithms in back-end verifiers and demonstrates the framework's practical application by instantiating it with elements of Viper and connecting it to two Viper back-ends and a front-end for concurrent separation logic. All technical results have been formalized in Isabelle/HOL, with artifacts available and evaluated as reusable.
