一句话：提出 LISSA，用专用求解器辅助惰性初始化，避免符号执行在堆输入上产生虚假符号结构。
符号执行难以分析处理堆分配输入的程序。惰性初始化通过从完全符号堆出发并按需初始化对象字段来支持这类输入，但当程序前置条件包含由 repOK 操作化描述的结构约束时，惰性初始化可能产生虚假的符号结构，使符号执行探索不可行路径并降低性能。已有方法依赖人工编写的规约来判断部分符号输入是否合法，以避免虚假结构，但开发者负担较高。LISSA 提出用专用求解器辅助惰性初始化，在按需初始化过程中借助专用求解机制判定部分符号结构的可行性，从而减少对人工规约的依赖，抑制虚假符号结构并改善符号执行。摘要未给出具体实验评估。
Programs that deal with heap-allocated inputs are difficult to analyze with symbolic execution (SE). Lazy Initialization (LI) is an approach to SE that deals with heap-allocated inputs by starting SE over a fully symbolic heap, and initializing the inputs’ fields on demand, as the program under analysis accesses them. However, when the program’s assumed precondition has structural constraints over the inputs, operationally captured via repOK routines, LI may produce spurious symbolic structures, making SE traverse infeasible paths and undermining SE’s performance. repOK can only decide the feasibility of fully concrete structures, and thus previous work relied on manually crafted specifications designed to decide the (in)validity of partially symbolic inputs, to avoid producing spurious symbolic structures. However, these additional specifications require significant further effort from the developers.
@inproceedings{paperbot7259,
title = {LISSA: Lazy Initialization with Specialized Solver Aid},
author = {Juan Manuel Copia and Pablo Ponzio and Nazareno Aguirre and Alessandra Gorla and Marcelo Frias},
booktitle = {ASE},
year = {2022},
doi = {10.1145/3551349.3556965}
}