Abstraction Discovery and Refinement for Model Checking by Symbolic Trajectory Evaluation