Abstract Debuggers: Exploring Program Behaviors Using Static Analysis Results
summary
Prototype debugger uses Goblint to let developers navigate an abstract reachability graph produced by a static analyzer, mapping debugger actions to abstract stepping operations and preserving soundness with a formal proof. The tool shows multiple context-sensitive abstract states per program point, supports step into/over/out/back, and lets users pick a context to trace why a data‑race warning appears. Demo traces an over‑approximation to a missed break that creates a spurious publish path; implementation and case studies show the idea is practical.
AI-written summary · about
chapters (12)
- 0:00Abstract debuggers concept
- 2:48Improving static analyzer usability
- 3:09Live demo of abstract debugger
- 5:59Theoretical background
- 7:46Formalizing debugger stepping
- 9:33Preserving soundness
- 10:19Concrete vs abstract debugger
- 11:44Abstract reachability graphs
- 12:46Configurable debugging framework
- 14:13Static analysis meets debuggers
- 15:21Conclusion and future work
- 17:13Q&A
related talks
37mThe Bright Future of Debuggers: Challenges and Opportunities
29mCross-Level Debugging for Static Analysers
14mDebugging debuggers!!!
18mPreview: Verification (Correctness & Debugging)
42mJava debugging tips & tricks
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
01h 01mBack to Basics: Debugging in Cpp
41mDebugger Driven Developement with Pry