Building Deductive Program Verifiers