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.

翻译：抽象解释通过系统抽象为构建可靠的静态分析提供了原理性基础。其核心挑战在于在给定抽象域内合成能够实现最优精度的最佳抽象转换器。本文针对以固定大小位向量建模的低级代码处理该问题。现有方法将合成任务建模为多目标优化模理论（OMT）问题，但存在可扩展性受限的缺陷。我们提出Spear并行合成框架，该框架利用一个关键结构洞见：虽然每个目标内的位必须顺序处理，但目标本身是相互独立的。Spear利用目标间位的独立性来更好地并行化合成过程。在覆盖两个二进制分析领域的基准测试上的实验结果表明，Spear始终优于最先进的OMT求解器，成功解决更多实例并显著缩短运行时间。据我们所知，这是首个应用并行性加速最优抽象转换器合成的方法。