Finding Bugs Using Path-Sensitive Static Analysis
summary
Path‑sensitive static analysis simulates execution, records path conditions and uses polyhedra‑based reasoning plus off‑the‑shelf solvers to prune infeasible paths and cut false positives. MSVC implements an access‑path store, a Fourier‑Motzkin style linear solver and a practical workflow that runs fast solvers first then uses constraint solver refutations (e g Z3) only for reported warnings. Exploration can explode exponentially so heuristics and concolic traces limit paths; checks ship in Visual Studio Community and as GitHub security actions.
AI-written summary · about
chapters (33)
- 0:00Intro
- 0:27Overview
- 0:57Welcome
- 1:25Agenda
- 2:53Static Analysis Tools
- 4:01Flow Insensitive Analysis
- 4:38Example
- 8:28Summary
- 9:15Resources
- 9:57PathSensitive Analysis
- 14:49Performance vs Precision
- 16:15Checks
- 16:39Future Talks
- 17:34Math
- 18:14Memory Layout
- 19:25Graphical Approach
- 20:18Alternative Approach
- 22:12Reasoning Values
- 23:46Polyhedra
- 26:54Skin elimination
- 27:32Rewriting inequalities
- 30:19A contradiction
- 31:17Eliminating inequalities
- 32:42Linear constraints
- 35:05Using a theorem prover
- 36:29Leveraging theorem provers
- 37:38When can PathSensitive Analysis go wrong
- 37:58Code snippet
- 38:11Error report
- 39:34Annotations
- 43:28Lessons Learned
- 46:34Conclusion
- 47:01Questions
related talks
36mCode Analysis: Empowering developers to write performant, reliable, and safe C++
44mStatic analysis as an additional barrier against bugs
09mModern Static Code Analysis the Example of PVS-Studio
18mSymbolic Execution Explained: Finding Bugs in Complex Code Paths
18mEnhancing Static Analysis for Practical Bug Detection: An LLM-Integrated Approach
38mStatic Code Analysis - A Behind-the-scenes Look
55mJava PathFinder: going to Mars without bugs and deadlocks
58mSecurity Static Analysis - Avoiding an Angry Mob of Engineers