Abstract: Program invariants play an important useful role in understanding programs as well as verifying properties about them. There are many ways to obtain program invariants--automatically, semi-automatically or they could be provided by a programmer as a part of a specification of the program or as annotations. The problem of determining whether a proposed formula is an invariant is undecidable. In this talk, methods are proposed to determine when in certain cases, formulas expressed in various logical theories can be determined to be invariant. If a formula is indeed an invariant, techniques for strengthening the formula to generate inductive invariants are explored.