Synthesizing Best Abstract Transformers via Parallel Bit-Vector Optimization
For developers of static analyses, Spear provides a faster method to synthesize optimal abstract transformers, addressing scalability issues in existing OMT-based approaches.
The paper introduces Spear, a parallel synthesis framework that exploits the independence of inter-objective bits to accelerate the synthesis of optimal abstract transformers for fixed-size bit-vectors, consistently outperforming state-of-the-art OMT solvers on benchmarks across two binary analysis domains.
Abstract interpretation provides a principled foundation for constructing sound static analyses through systematic abstraction. A central challenge is synthesizing the best abstract transformers that achieve optimal precision within a given abstract domain. This paper addresses this problem for low-level code modeled with fixed-size bit-vectors. Recent approaches formulate the synthesis task as a multi-objective Optimization Modulo Theories (OMT) problem, but suffer from limited scalability. We introduce Spear, a parallel synthesis framework that exploits a key structural insight: while the bits within each objective must be processed sequentially, the objectives themselves are independent. Spear leverages the independence of inter-objective bits to better parallelize the synthesis. Experimental results on benchmarks across two binary analysis domains show that Spear consistently outperforms state-of-the-art OMT solvers, solving more instances and achieving significantly improved runtimes. To our knowledge, this is the first approach to apply parallelism to accelerate the synthesis of optimal abstract transformers.