Interprocedural Shape Analysis Using Separation Logic-Based Transformer Summaries
summary
Proposes using connectors from separation logic to encode abstract transformation relations as procedure summaries, then composes them top-down to avoid reanalyzing callees. Implements three Frama‑C plugins (state, relational, and summary-based) and evaluates on shape-bearing C code: summaries are often reusable so many functions get reanalyzed at most three times, the compositional analysis matches state analysis precision in most cases and runs faster overall, and the contextual procedure summary plus the frame rule enable sparse, precise memory effects.
AI-written summary · about
chapters (24)
- 0:00Introduction
- 0:21State vs transformation goals
- 1:23Interprocedural analysis with summaries
- 2:48Abstract transformation for state
- 3:52Shape analysis with separation logic
- 5:00Interprocedural contribution focus
- 5:20Example: linear equalities abstraction
- 6:42Abstract transformation components
- 8:09Abstract composition of transformations
- 9:41Global summary limitations
- 11:08Context summaries for precision
- 13:19Need for context and transformation
- 15:04Top-down algorithm overview
- 16:29Extending to relational logic
- 18:16Separating memory and numerical domains
- 19:41Generalizing memory representations
- 20:06Analyzer implementation and evaluation
- 21:52Key takeaways
- 22:59Q&A: Separation logic choice
- 24:44Q&A: Context for summaries
- 25:50Q&A: Recomputing summaries
- 26:31Q&A: Beyond shape analysis
- 28:05Q&A: Verification vs proof
- 29:12Q&A: Algorithm convergence
related talks
19mProof Automation for Linearizability in Separation Logic
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
15mAutomatic Synthesis of Data-Flow Analyzers
14mTowards Cumulative Abstract Semantics via Handlers (Short Paper)
52mThink Abstractly, Work Concretely
05mNew foundations for probabilistic separation logic
17mExploiting the Sparseness of Control-Flow and Call Graphs for Efficient and On-...
22mA Categorical Basis for Robust Program Analysis