Symbolic execution is at the core of many techniques for program analysis and test generation. Traditional symbolic execution of programs with numeric inputs enjoys the property of forking as many analysis traces as the number of analyzed program paths, a property that in this paper we refer to as path optimality. On the contrary, current approaches for symbolic execution of heap-manipulating programs fail to satisfy this property, thereby incurring crucial path explosion effects. This paper introduces POSE, path-optimal symbolic execution, a symbolic execution algorithm that originally achieves path optimality against heap-manipulating programs. We formalize the POSE algorithm and experiment it against a benchmark of programs that take data structures as inputs, supporting the potential of POSE for improving on the state of the art of symbolic execution of heap-manipulating programs.

翻译：符号执行是程序分析和测试生成诸多技术的核心。针对数值输入程序的传统符号执行具有生成与所分析程序路径数量相等的分析轨迹的特性，本文称之为路径最优性。相反，当前堆操作程序的符号执行方法均无法满足此特性，从而导致严重的路径爆炸效应。本文提出路径最优符号执行算法POSE，该算法首次实现对堆操作程序的路径最优性。我们形式化描述了POSE算法，并在以数据结构为输入的程序基准测试集上进行实验，结果验证了POSE在改进堆操作程序符号执行技术现状方面的潜力。