Quantifying the Exploration of the Korat Solver for Imperative Constraints

Tools that explore very large state spaces to nd bugs, e.g., when model checking, or to nd solutions, e.g., when constraint solving, can take a considerable amount of time before the search termi- nates, and the user may not get useful feedback on the state of the search during that time. Our focus is a tool that solves im- perative constraints to provide automated test input generation for systematic testing. Speci cally, we introduce a technique to quantify the exploration of Korat, a well-known tool that explores the bounded space of all candidate inputs and enumerates desired inputs that satisfy given constraints. Our technique quanti es the size of the input space as it is explored by the Korat search, and provides the user exact information on the size of the remaining input space. In addition, it allows studying key characteristics of the search, such as the distribution of solutions as the search nds them. We implement the technique as a listener for the Korat search, and present initial experimental results using it.