一句话：利用一阶公式中的区间与数据依赖信息加速 eager SMT 求解中的位向量可满足性判定。
SMT 求解是符号程序分析等技术的常见性能瓶颈，eager SMT 求解通过将一阶公式归约为纯布尔公式并交给 SAT 求解器判定可满足性。然而，如何让 SAT 求解器利用一阶公式中的结构化知识仍不清楚。本文提出一种新的快速方法，从一阶公式中学习区间信息和数据依赖信息，并将其用于提升 eager SMT 求解效率。摘要未报告具体实验设置与量化结果，核心贡献在于面向位向量可满足性的知识增强求解思路。
SMT solving is often a major source of cost in a broad range of techniques such as symbolic program analysis. Thus, speeding up SMT solving is still an urgent requirement. A dominant approach, which is known as eager SMT solving, is to reduce a first-order formula to a pure Boolean formula, which is handed to an expensive SAT solver to determine the satisfiability. We observe that the SAT solver can utilize the knowledge in the first-order formula to boost its solving efficiency. Unfortunately, despite much progress, it is still not clear how to make use of the knowledge in an eager SMT solver. This paper addresses the problem by introducing a new and fast method, which utilizes the interval and data-dependence information learned from the first-order formulas.
DOI 原文 ·
@inproceedings{paperbot6034,
title = {Fast bit-vector satisfiability},
author = {Peisen Yao and Qingkai Shi and Heqing Huang and Charles Zhang},
booktitle = {ISSTA},
year = {2020},
doi = {10.1145/3395363.3397378}
}