This paper describes the Korat tool for constraint-based generation of
structurally complex test inputs for Java programs. Korat takes (1) an
imperative predicate that speci fies the desired structural integrity
constraints and (2) a finitization that bounds the desired test input
size. Korat generates all inputs (within the bounds) for which the
predicate returns true. To do so, Korat performs a systematic search
of the predicate's input space. The inputs that Korat generates enable
bounded-exhaustive testing for programs ranging from library classes
to stand-alone applications.