一句话：提出多区间理论求解器 PARTI，加速符号执行中特定结构的数组与位向量查询，非该结构时回退完整求解器。
符号执行是一种有效的程序分析技术，但其可扩展性在很大程度上取决于快速求解大量一阶逻辑查询的能力。本文提出 PARTI，一种多区间理论求解器，用于加速数组与位向量理论中具有特定结构的查询求解；对于不符合该结构的查询，则回退到完整求解器。该方法的目标是在保持一般情形完备性的同时，提升此类特殊结构查询的求解效率。摘要未报告具体实验数据或量化结果，因此其评估细节未在摘要中说明。
Symbolic execution is an effective program analysis technique whose scalability largely depends on the ability to quickly solve large numbers of first-order logic queries. We propose an effective general technique for speeding up the solving of queries in the theory of arrays and bit-vectors with a specific structure, while otherwise falling back to a complete solver.
DOI 原文 ·
@inproceedings{paperbot4696,
title = {PARTI: a multi-interval theory solver for symbolic execution},
author = {Oscar Soria Dustmann and Klaus Wehrle and Cristian Cadar},
booktitle = {ASE},
year = {2018},
doi = {10.1145/3238147.3238179}
}