Cross-Level Debugging for Static Analysers
summary
A cross-level debugger is implemented inside the MAF framework that moves breakpoints into the analyzed program and evaluates meta-predicates (store, lce, work-list) via a separate predicate evaluator. It provides history-aware, domain-specific conditional breakpoints that pause the abstract interpreter without changing analysis state. Validation reintroduces four real bugs plus a synthetic one from MAF’s repo and shows concrete wins: e.g. reducing breakpoint suspensions from 16 to 6 to pinpoint a non-termination due to mistaken component reanalysis.
AI-written summary · about
chapters (14)
- 0:00Static analysis debugging intro
- 2:29Debugging static analysers challenges
- 5:43Abstract interpretation
- 8:11Non-determinism in execution
- 8:54Modular analysis dependencies
- 11:04Cross-level debugger interface
- 12:49Conditional breakpoints explained
- 15:24Breakpoint evaluation
- 16:49Debugger validation method
- 17:54Case study: non-termination bug
- 21:50Conditional breakpoints effectiveness
- 22:34Future work
- 23:16Conclusion
- 23:57Q&A
related talks
21mAbstract Debuggers: Exploring Program Behaviors Using Static Analysis Results
18mPreview: Verification (Correctness & Debugging)
14mDebugging debuggers!!!
31mAnICA: Analyzing Inconsistencies in Microarchitectural Code Analyzers
18mEnhancing Static Analysis for Practical Bug Detection: An LLM-Integrated Approach
52mFinding Bugs Using Path-Sensitive Static Analysis
36mCode Analysis: Empowering developers to write performant, reliable, and safe C++
40mDebugging Elixir Code - The Tools, The Mindset