一句话：提出在 SMT 求解中利用程序控制流知识剪枝搜索空间，显著提升程序验证效率。
SMT 求解器已广泛用作各类软件分析与验证技术的推理引擎，其效率直接影响这些技术的性能。然而现有求解器面向通用约束求解设计，无法利用程序中大量有用的结构信息，导致在冗余搜索空间上耗费大量开销。本文提出一种在 SMT 求解中利用控制流知识的新方法，将程序控制流信息引入求解过程以引导搜索、剪枝冗余空间。作者在可信基准上进行了大量实验，结果表明该方法可将求解效率提升数个数量级。
Satisfiability modulo theories (SMT) solvers have been widely applied as the reasoning engine for diverse software analysis and verification technologies. The efficiency of the SMT solver has significant effects on the performance of these technologies. However, the current SMT solvers are designed for the general purpose of constraint solving. Many useful knowledge of programs cannot be utilized during the SMT solving. As a result, the SMT solver may spend a lot of effort to explore redundant search space. In this paper, we propose a novel approach for utilizing control-flow knowledge in SMT solving. With this technique, the search space can be considerably reduced and the efficiency of SMT solving is observably improved. We conducted extensive experiments on credible benchmarks, the results show orders of magnitude improvements of our approach.
DOI 原文 ·
@inproceedings{paperbot4768,
title = {Control flow-guided SMT solving for program verification},
author = {Jianhui Chen and Fei He},
booktitle = {ASE},
year = {2018},
doi = {10.1145/3238147.3238218}
}