Competent predicate abstraction in model checking

The paper presents a new approach to computing the abstract state and a maximum weight heuristicmethod for finding the shortest counter-example in verification of imperative programs. The strategy isincorporated in a verification system based on the counterexample-guided abstraction refineme