一句话：提出两阶段符号执行方法，用深度学习合成程序特定求解策略以提升约束求解性能。
约束求解是符号执行的主要瓶颈之一。现代 SMT 求解器允许用户通过求解策略定制内部求解过程。本文（扩展摘要）报告了为给定程序合成程序特定求解策略的近期进展。作者提出两阶段符号执行流程：第一阶段利用深度学习技术合成求解策略；第二阶段在符号执行中应用该策略，以改善约束求解性能。初步实验结果表明该方法具有潜力。由于是扩展摘要，文中未展开完整技术细节与大规模评估。
Constraint solving is one of the challenges for symbolic execution. Modern SMT solvers allow users to customize the internal solving procedure by solving strategies. In this extended abstract, we report our recent progress in synthesizing a program-specific solving strategy for the symbolic execution of a program. We propose a two-stage procedure for symbolic execution. At the first stage, we synthesize a solving strategy by utilizing deep learning techniques. Then, the strategy will be used in the second stage to improve the performance of constraint solving. The preliminary experimental results indicate the promising of our method.
DOI 原文 ·
@inproceedings{paperbot5871,
title = {Synthesizing smart solving strategy for symbolic execution},
author = {Zehua Chen and Zhenbang Chen and Ziqi Shuai and Yufeng Zhang and Weiyu Pan},
booktitle = {ASE},
year = {2020},
doi = {10.1145/3324884.3418904}
}