Abstracting models from execution traces for performing formal verification