Verification-Preserving Inlining in Automatic Separation Logic Verifiers
summary
Presents a provable criterion that makes bounded inlining safe for automatic separation-logic verifiers: a semantic condition (formalized in Isabelle/HOL) that guarantees verification-preserving inlining and a weaker syntactic structural condition that the tool checks automatically. Implements the checker in Viper, evaluates on >1,500 benchmark files, manually samples 72 files (22 show non-preserving inlining), and reports that the semantic condition captures 49/50 and the structural check 47/50 of cases where inlining remains safe; artifacts are available.
AI-written summary · about
chapters (10)
- 0:00Separation logic verification
- 1:46Bounded verification motivation
- 3:10Inlining as solution
- 4:12Problem with inlining
- 7:48Key problem in verifiers
- 8:29Paper contributions
- 9:53Semantic condition
- 13:06Evaluation results
- 14:52Summary
- 15:32Question and answer session
related talks
28mGradual Verification: Assuring Software Incrementally
01h 05mVerifying Infinitely Many Programs at Once
18mWP-Preserving Compilation -- Preserving Weakest Preconditions For End-to-End Verification
19mPredictable Verification using Intrinsic Definitions
21mEmbedding Hindsight Reasoning in Separation Logic
21mMechanised Hypersafety Proofs about Structured Data
13mRevealing Sources of (Memory) Errors via Backward Analysis
26mUnfolding Expressions for Gradual Verification