Automatic understanding of the intended meaning of computer programs is a very hard problem, requiring intelligence and reasoning. In this abstract we discuss a new method for program analysis, called symbol elimination. Symbol elimination uses first-order theorem proving techniques to automatically discover non-trivial program properties, such as loop invariants and loop bounds. Moreover, symbol elimination can be used as an alternative to interpolation for software verification.