Scalable and Precise Static Analysis
← Back to homepage
Static analysis detects software bugs without executing the program. My work focuses on making these techniques both scalable to millions of lines of code and precise enough to produce actionable results with low false positive rates.
Abstract Interpretation
Abstract interpretation computes sound over-approximations of program behaviors. My work addresses key challenges in making it practical for large codebases:
- Cross-domain sparse abstract execution — We proposed CSA, a framework enabling online bidirectional refinement between memory address and interval domains via implication-equivalent correlation tracking, achieving ~2.5x speedup and 96% false positive reduction on real-world projects.
[C5: ICSE '24]
- Selective widening — We proposed SiftAbs, which uses value-flow cycle analysis to selectively apply widening only where needed, reducing widening variables by up to 99.5% and analysis time by up to 41% while maintaining identical precision.
[C10: OOPSLA '25]
- Recursive program analysis — We proposed RecTopo, an interprocedural weak topological ordering technique that partitions programs to eliminate spurious interprocedural cycles, achieving 95% precision on recursive programs (vs ~52% for baselines).
[C9: ECOOP '25]
Typestate Analysis
Typestate analysis verifies that objects follow correct API usage protocols (e.g., a file must be opened before reading and closed after use).
- Graph simplification for path-sensitive typestate analysis — We proposed FGS, a tempo-spatial multi-point slicing technique that reduces ICFG nodes by 89% as preprocessing, achieving 116x speedup and detecting 105 real bugs in 10 open-source projects with 82% precision. This work received the ACM SIGSOFT Distinguished Paper Award.
[C6: FSE '24]
Pointer Analysis and Specification Inference
Pointer analysis determines what memory locations a pointer may reference, which is foundational for many downstream analyses.
- Flow-sensitive pointer analysis without CFG — We proposed an efficient Andersen-style flow-sensitive pointer analysis that avoids constructing a full control flow graph.
[P1: arXiv]
- LLM-driven API specification generation — We proposed SpecGuru, which uses LLMs with bottom-up inference and differential testing-based self-validation to generate points-to specifications for library APIs, achieving 91% precision and 89% recall across 15 C libraries.
[C11: ICSE '26]
Quantum-Accelerated Analysis
- Quantum speedups for transitive closure-based analysis — We proposed the first truly subcubic quantum-accelerated framework for CFL-reachability and set constraint solving, reducing complexity from O(N3) to O(N2.5 · polylog(N)) using Grover's algorithm.
[J3: TOSEM '24]
← Back to homepage