SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025

Static analysis consists of a large body of tools that analyze programs without running them. Despite substantial progress in recent years, both theoretical and practical, static analyses still face bottlenecks in SMT solving, equivalence checking, and compiler verification. This work proposes alleviating these bottlenecks by using information derived from existing compilers, and asks whether such information is enough to inform static analysis and expand the set of tractable problems. We plan to investigate the problem by instrumenting a compiler to provide transformation records, which record of the analyses and optimizations a compiler performs on a particular input program. In existing work, we find that the strategy is promising by showing that compiler information can speed up SMT solving. Our proposal is to extend the work to a general instrumentation and filtering framework and evaluate it on translation validation and other use cases.