Invariante Synthese für unvollständige Verifikations-Engines