Constraint prioritization for efficient test generation using Korat

A key problem in software testing is generating a set of test cases which check for a variety of behaviors of a given software system. For testing programs that take inputs that are structurally complex it is imperative to come up with a way to increase efficiency for generating these complex structures. We take an existing algorithm for test case generation, Korat, and show how to improve its performance using constraint prioritization. The technique used in Korat is to perform bounded exhaustive testing using state space exploration to generate non-isomorphic structures. Korat uses a predicate method written by user which defines constraints for the desired data structure. We describe a technique for re-writing the predicate method to enable Korat to generate tests more efficiently.