Automatic Invariant Generation

Program invariants are statements or assertions that are widely used in program analysis and proving correctness of programs. A program invariant can be defined for every program location. Invariants provide properties that hold for every valid program execution, and are crucial in program verification. In this survey, we shall describe some techniques that have been used in the past to generate invariants by analyzing programs.