Loop invariants play a central role in ensuring the reliability of software. Program analysis techniques must either require such program annotations at appropriate program locations or automatically derive these annotations from a program. A new approach for automatically generating loop invariants from imperative programs will be presented. Loop invariants are assumed to have certain shape, i.e., they are formulas in a restricted quantifier-free first-order theory. Elimination techniques can be used to generate such invariants. The focus of this talk will be on exploring heuristics for quantifier-elimination so that such techniques can scale well. A nice feature of the proposed approach is that it does not need to have access to any specification or annotations associated with a program. Some preliminary ideas about how to generalize these approaches to work on data types other than numbers will be discussed.
