Goal-Directed Abstract Interpretation and Event-Driven Frameworks

on YouTube ↗56m

" summary

Argues for goal-directed backward analysis that models only callbacks relevant to a single error, implements abstract message histories to represent realizable framework-app traces, and ships a prototype Historia that proved all 5 real bug/fix pairs (distinguishing buggy vs fixed) by writing a handful of temporal specs. Evaluation covers 47 Android apps (~2M LOC), finds 190 candidate sites, and shows 43% provable without modeling while targeted specs (≤4 per case) verify additional cases and uncover one true bug.

AI-written summary · about

" chapters (14)

1. 0:00Introduction
2. 1:04Static analysis for Android apps
3. 9:58Event-driven framework challenges
4. 15:16Goal-directed abstract interpretation
5. 18:24Modeling missing transitions
6. 21:13Android framework limits
7. 24:48Framework-app interface
8. 29:40Model for D-reference safety
9. 35:17Callback control flow fix
10. 44:12Evaluation on Android apps
11. 47:22Large-scale Android applications
12. 48:46Key ideas
13. 49:48Future directions
14. 50:40Q&A