Path-optimal symbolic execution of heap-manipulating programs

符号执行是许多程序分析和测试生成技术的核心。传统的对数值输入程序的符号执行具有分叉的特性，即分叉出与分析程序路径数相同的分析轨迹，这种特性在本文中被称为路径最优性。相反，当前符号执行堆操作程序的方法未能满足这种特性，从而导致路径爆炸效应，严重影响分析的效率。本文介绍了POSE（路径最优符号执行），一种符号执行算法，最初针对堆操作程序实现了路径最优性。我们为一种小型但具有代表性的面向对象编程语言形式化了POSE算法，并将该形式化实现为原型符号执行器，以实验算法对以数据结构为输入的样例程序的效果。我们的实验提供了初步的经验证据，证明了POSE在改进符号执行堆操作程序的现有技术方面的潜力。

本论文旨在解决堆操作程序的符号执行中存在的路径爆炸问题，提出了一种路径最优符号执行算法POSE。

POSE算法实现了堆操作程序的路径最优，通过对一个小型但代表性的面向对象编程语言的形式化描述，将其实现为原型符号执行器，并在数据结构作为输入的样例程序基准测试中进行了实验，初步证明了POSE算法改进堆操作程序符号执行的潜力。

本论文的亮点包括提出了一种解决路径爆炸问题的符号执行算法POSE，通过实验初步验证了POSE算法的有效性，为改进堆操作程序的符号执行提供了新思路。

在这个领域的相关研究包括：《KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs》、《DART: Directed Automated Random Testing》、《An Overview of Symbolic Execution for Software Testing》等。