符号执行中的约束求解问题研究进展

摘要

在符号执行中,约束求解主要负责路径可达性进行判定及测试输入生成的工作,但路径爆炸问题带来的频繁调用,以及SMT求解器本身的能力和效率的不足,使得约束求解占用了符号执行中主要的性能开销,约束求解问题也成为符号执行中面临的主要瓶颈问题之一.本文介绍了符号执行和约束求解的基本概念,并分析了符号执行中约束求解问题的由来,对近年来的约束求解问题研究进展进行了归类,涉及的技术包括非相关约束分支切片、约束简化、快速不满足性检查及多求解器支持等.对这方面的研究进行了展望和总结.提出未来工作应在提高路径约束逻辑精简率、提高约束求解结果存储和重用的效率、约束求解并行化以及约束求解配置预测等方面展开.