Backward-Korat : improving Korat search to enable backward input space exploration

Automated test input generation plays an important role in increasing
software quality. Exhaustively testing a program for all test inputs within a given bound helps check many corner cases that are easy to miss otherwise. Korat is a constraint solver and an automated testing framework for bounded exhaustive testing of Java programs. Korat uses a predicate method that describes desired inputs and a finitization bound to explore the space of all candidate inputs and generates the desired ones. Korat performs a systematic backtracking search for input space exploration based on pruning and isomorphism breaking. The Korat search gains part of its efficiency by monitoring executions of the given predicate on candidate inputs and creating new candidates based on the object fields accessed by the predicate during its execution. The Korat search has a default order for exploring the candidate inputs -- the search always performs the same exploration for the same predicate and finitization.

Our thesis is that a different search order for the Korat search can enhance the efficacy of Korat. Specifically, we introduce the backward Korat, a novel approach to enable Korat to go backward in the search space. Our technique is built on the core of the traditional Korat search. The backward Korat can be applied to a variety of existing techniques including constraint-based data structure repair, parallel Korat, etc. We evaluate our approach using a standard suite of data structures. The experimental results show that the backward search works well and generates the same test inputs as the traditional search produces even though it performs slower compared to the forward search. Using the backward search and the traditional Korat search in tandem enables a new set of possible applications.