Constructive Methods in Automatic Analysis of Correctness Proofs