Modern software pervasively uses structurally complex data such as linked data structures. The standard approach to generating test suites for such software, manual generation of the inputs in the suite, is tedious and error-prone. This talk presents Korat, a new technique that automates the generation of suites with structurally complex test inputs. Korat allows the developer to describe the properties of valid inputs using a familiar implementation language such as Java. Given a description and a bound on the input size, a Korat tool automatically generates the test suite.

Korat tools have been implemented and used in both academia and industry. Developers typically use these tools to generate bounded-exhaustive test suites that contain all nonequivalent inputs up to a given size. Our results show that this approach provides high-quality test suites that achieve excellent code coverage for data-structure libraries. Moreover, developers have successfully used this approach to discover errors in real applications, including a naming architecture for networks, a solver for declarative predicates, a fault-tree analyzer, and several tools for XML languages.