Efficient State Merging in Symbolic Execution

Symbolic execution has proven to be a practical technique for building automated test case generation and bug finding tools. Nevertheless, due to state explosion, these tools still struggle to achieve scalability. Given a program, one way to reduce the number of states that the tools need to explore is to merge states obtained on different paths. Alas, doing so increases the size of symbolic path conditions (thereby stressing the underlying constraint solver) and interferes with optimizations of the exploration process (also referred to as search strategies). The net effect is that state merging may actually lower performance rather than increase it. We present a way to automatically choose when and how to merge states such that the performance of symbolic execution is significantly increased. First, we present query count estimation, a method for statically estimating the impact that each symbolic variable has on solver queries that follow a potential merge point; states are then merged only when doing so promises to be advantageous. Second, we present dynamic state merging, a technique for merging states that interacts favorably with search strategies in automated test case generation and bug finding tools. Experiments on the 96 GNU COREUTILS show that our approach consistently achieves several orders of magnitude speedup over previously published results. Our code and experimental data are publicly available at http://cloud9.epfl.ch.


Published in:
Acm Sigplan Notices, 47, 6, 193-204
Year:
2012
Publisher:
New York, Assoc Computing Machinery
ISSN:
0362-1340
Keywords:
Laboratories:




 Record created 2013-02-27, last modified 2018-03-17


Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)