Historia: Refuting Callback Reachability with Message-History Logics
summary
Defines message histories (sequences of boundary call-ins/callbacks) and a temporal message-history logic, implements a prototype verifier called Historia that combines backwards goal-directed analysis with SMT solving in an extended EPR fragment, and automates an excludes initial check to rule out unrealizable framework behaviors. Empirically distinguishes buggy vs fixed on five real issues, reaches fixpoints after ~3–5 callbacks, analyzes 47 apps (2M LOC), proves 43% of sites safe within an hour and finds one true bug.
AI-written summary · about
chapters (14)
- 0:00Program analysis intro
- 0:23Historia research motivation
- 1:26Android crash root cause
- 3:13Message histories in Android
- 5:01Framework code analysis challenges
- 6:09Control flow with message histories
- 6:53Call-Temporal Logic for behavior
- 7:58Automating proofs with SMT
- 8:40Backwards analysis of histories
- 11:27Unrealizable framework behavior
- 12:35Reasoning with equality
- 13:17Empirical evaluation on apps
- 15:02Scaling to 47 apps
- 16:08Q&A
related talks
21mAbstract Debuggers: Exploring Program Behaviors Using Static Analysis Results
23mSpecifying and Verifying Future Conditions
01h 05mVerifying Infinitely Many Programs at Once
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
17mReasoning about External Calls
14mA Hoare Logic For Symmetry Properties
36mRethinking legacy modernisation with automated reasoning and comprehension models
27mLet's Bring System Dynamics Back to CS!