Guided Dynamic Symbolic Execution Using Subgraph Control-Flow Information.

Dynamic symbolic execution (DSE) is an efficient SMT-based path enumeration technique used in software testing. In this work in progress, we consider here the case of guided DSE, where the paths to enumerate should be part of a given program slice. We propose a new path selection criterion, which aims to minimize the number of queries to the SMT solvers. This criterion is based on the probability of a path to exit the program slice. Experiments show that this information can be computed in a reasonable time for DSE purpose.