一句话：提出分段内存模型，缓解符号执行处理复杂堆结构时因指针可指向多个对象而大量分叉的问题。
符号执行能有效探索程序路径并对路径上的所有可能取值进行推理，但在处理复杂堆数据结构时仍面临困难：当指针可能指向多个内存对象时，符号执行通常需要为每个可能对象分叉出不同状态，导致状态爆炸。本文提出一种用于符号执行的分段内存模型（segmented memory model），其目标是通过新的堆内存组织方式避免或减少这种逐对象分叉。给出的摘要仅描述了上述问题动机，未展开模型的具体定义、实现机制或实验评估结果，因此无法从摘要判断其相对已有方法的实际收益。
Symbolic execution is an effective technique for exploring paths in a program and reasoning about all possible values on those paths. However, the technique still struggles with code that uses complex heap data structures, in which a pointer is allowed to refer to more than one memory object. In such cases, symbolic execution typically forks execution into multiple states, one for each object to which the pointer could refer.
DOI 原文 ·
@inproceedings{paperbot5117,
title = {A segmented memory model for symbolic execution},
author = {Timotej Kapus and Cristian Cadar},
booktitle = {FSE},
year = {2019},
doi = {10.1145/3338906.3338936}
}