Synthesizing Best Abstract Transformers via Parallel Bit-Vector Optimization
2026-06-15 • Programming Languages
Programming Languages
AI summaryⓘ
The authors focus on improving how computer programs analyze low-level code by creating better rules that help catch errors more accurately. They introduce Spear, a new system that speeds up this process by working on independent parts of the problem at the same time, instead of one after the other. Tests show that Spear is faster and solves more problems than previous methods. This work is the first to use parallel computing to make this kind of analysis synthesis more efficient.
abstract interpretationstatic analysisabstract transformersbit-vectorsOptimization Modulo Theories (OMT)parallel synthesisbinary analysisprogram analysisprecisionscalability
Authors
Weiqi Wang, Peisen Yao, Hanrui Zuo, Yuan Li, Hongfei Fu, Kui Ren
Abstract
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.