Comparing Abstraction Refinement Algorithms

AbstractWe present a generic algorithm that provides a unifying scheme for the comparison of abstraction refinement algorithms. It is centered around the notion of refinement cue which generalizes counterexamples. It is demonstrated how the essential features of several refinement algorithms can be captured as instances.We argue that the generic algorithm does not limit the completeness of instances, and show that the proposed generalization of counterexamples is necessary for completeness — thus addressing a shortcoming of more limited notions of counterexample-guided refinement