Welcome to Korat Home Page
Korat is a tool for constraint-based generation of structurally complex test inputs for Java programs. Structurally complex means that the inputs are structural (e.g., represented with linked data structures) and must satisfy complex constraints that relate parts of the structure e.g., invariants for linked data structures).
Korat requires (1) an imperative predicate that specifies the desired structural constraints and (2) a finitization that bounds the desired test input size. Korat generates all predicate 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.
Korat can graphically show the structures it generates. The visualization in Korat was inspired by Alloy, and our current Korat implementation uses the Alloy Analyzer's visualization facility, which provides a fully customizable display that allows users to specify desired views on the underlying structures. Korat automatically translates object graphs into the Alloy representation.
You may take a look at Google Tech Talk presentation describing Korat on YouTube.