Three-valued abstraction and heuristic-guided refinement for verifying concurrent systems