When to Stop Going Down the Rabbit Hole: Taming Context-Sensitivity on the Fly
summary
Provides a framework and three generic lifters implemented as decorators around Goblint and evaluated on SV-COMP recursive benchmarks. Limits contexts on the fly without pre-analysis and reuses existing analyses unchanged. Reduces stack overflows and timeouts compared to full context; context gas (initial value 30) raises correct no-overflow verdicts by 31%. Context widening and loop-free call string remove resource failures but trade off precision.
AI-written summary · about
chapters (12)
- 0:00Context-sensitive analysis intro
- 2:57Goal of dynamic limits
- 5:07Three approaches to tame
- 9:05Context gas limits recursion
- 12:04Experimental results on tasks
- 15:15Conclusion and future
- 16:29Q&A: Loop-free precision loss
- 17:52Q&A: Access path precision loss
- 19:39Q&A: Call string vs context gas
- 20:42Q&A: Reanalysis with gas values
- 21:44Q&A: Gas vs unrolling
- 22:26Q&A: Non-determinism in results
related talks
26mA Beginners Guide to Context
55mCharting the uncharted: Discovering and evolving bounded contexts
51mDissecting Bounded Contexts -
07mHow Should We Access Global Resources?
42mBounded Context: Keep It Simple!
21mMutual Refinements of Context-Free Language Reachability
17mContextual Equality Saturation
51mStretching the Glasgow Haskell Compiler: Nourishing GHC with Domain-Driven De...