Exploiting hub states in automatic verification