Verifying safety properties using separation and heterogeneous abstractions