A Constructive Approach to Static Verification of Program Properties