SCSE: Boosting Symbolic Execution via State Concretization

Huibin WANG  Chunqiang LI  Jianyi MENG  Xiaoyan XIANG  

IEICE TRANSACTIONS on Information and Systems   Vol.E102-D   No.8   pp.1506-1516
Publication Date: 2019/08/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.2018EDP7298
Type of Manuscript: PAPER
Category: Software Engineering
state concretization,  symbolic execution,  constraint solving,  

Full Text: PDF(516.4KB)>>
Buy this Article

Symbolic execution is capable of automatically generating tests that achieve high coverage. However, its practical use is limited by the scalability problem. To mitigate it, this paper proposes State Concretization based Symbolic Execution (SCSE). SCSE speeds up symbolic execution via state concretization. Specifically, by introducing a concrete store, our approach avoids invoking the constraint solver to check path feasibility at conditional instructions. Intuitively, there is no need to check the feasibility of a path along a concrete execution since it is always feasible. With state concretization, the number of solver queries greatly decreases, thus improving the efficiency of symbolic execution. Through experimental evaluation on real programs, we show that state concretization helps to speed up symbolic execution significantly.