Automatic induction proofs of data-structures in imperative programs