Daikon

Daikon is an implementation of dynamic detection of likely invariants; that is, the Daikon invariant detector reports likely program invariants. An invariant is a property that holds at a certain point or points in a program; these are often seen in assert Statements, documentation, and formal specifications. Invariants can be useful in program understanding and a host of other applications. Examples include