Interprocedural Shape Analysis Using Separation Logic-Based Transformer Summaries

on YouTube ↗20m

" summary

Builds context-sensitive procedure summaries as relational transformations over separation logic (pairs of input/output heap descriptions h# and t#), implemented as a Frama-C plug-in and applied to ~2k lines of Emacs C. Composition and widening produce summaries (including for recursion) that preserve precision on the benchmark; summary-based analysis runs about 60× faster than state inlining and 300× faster than relational inlining. Uses relational separation logic and reports no observed precision loss.

AI-written summary · about

" chapters (18)

1. 0:00Memory analysis with separation logic
2. 1:05Transformation analyses and summaries
3. 2:12Abstract transformations vs inlining
4. 3:22Composing abstract transformations
5. 6:01Interprocedural transformation analysis
6. 6:23Shape abstract transformation composition
7. 8:18Soundness of composition
8. 8:39Example of composition
9. 10:16Interprocedural relational analysis
10. 10:37Context transformation summaries
11. 12:34Context and transformation needs
12. 12:58Applying summaries
13. 15:02Insufficient summary contexts
14. 16:08Frama-C implementation
15. 16:54Emacs code evaluation
16. 17:59Performance gains
17. 18:22Precision and verification
18. 18:43Conclusion