Abstraction discovery and refinement for model checking by symbolic trajectory evaluation - Adams, S (University of Oxford, 2014)