符号执行中带量词的状态合并
软件工程
2023-08-25 v2
摘要
我们解决约束编码爆炸问题，该问题阻碍了状态合并在符号执行中的适用性。具体而言，我们的目标是减少状态合并过程中引入的析取与 if-then-else 表达式的数量。核心思想是依据路径约束中检测到的相似统一结构，将符号状态动态划分为合并组，从而利用量词高效编码合并后的路径约束与内存。为应对量化约束求解增加的复杂性，我们提出一种专用求解流程，在许多情况下缩短了求解时间。我们的评估表明，该方法可带来显著的性能提升。
引用
@article{arxiv.2308.12068,
title = {State Merging with Quantifiers in Symbolic Execution},
author = {David Trabish and Noam Rinetzky and Sharon Shoham and Vaibhav Sharma},
journal= {arXiv preprint arXiv:2308.12068},
year = {2023}
}