Verification-Preserving Inlining in Automatic Separation Logic Verifiers

Explore a 20-minute conference talk from OOPSLA1 2023 that delves into verification-preserving inlining techniques for automatic separation logic verifiers. Learn about the challenges of bounded verification in detecting bugs and ensuring program correctness. Discover how the researchers developed a novel approach to address issues with inlining in separation logic verifiers like Caper, GRASShopper, RefinedC, Steel, and VeriFast. Understand the semantic condition identified and proven in Isabelle/HOL that ensures verification-preserving inlining. Examine the dual result demonstrating how successful verification of inlined programs relates to the original program's verification. Gain insights into the automatic checking methods for the semantic condition, including syntactic and program verifier-based approximations. See the implementation of these checks in Viper and their effectiveness on non-trivial examples from various verifiers. Access supplementary materials and explore the implications of this research for modular verification, bounded verification, inlining, and loop unrolling in program analysis.