符号执行中约束求解结果重用技术的比较

约束求解耗时一直是符号执行的瓶颈之一,约束求解结果重用是一种有效提高符号执行效率的方法。本文对约束求解重用技术Green、Klee-R、GreenTrie及Green、Utopia进行比较,证明了前三者重用能力从高到低依次是GreenTrie,Klee-R,Green,后两者中Utopia的重用能力高于Green。在动态符号执行场景下对四种重用方法的重用效率进行了实验比较,证明重用技术的重用效率并不完全取决于重用能力,并进一步从程序的特点、约束的类型以及约束的次序对重用效率的影响进行了分析和比较。本文的工作为约束求解重用领域的研究提供了综述和评估,可以为未来该领域的研究提供借鉴。