CEGAR (Counter-Example Guided Abstraction Refinement)

[Google Scholar] [Wikipedia]

Papers: clarke:cav:2000

Counter-Example Guided Abstraction Refinement is a method of constructing an abstraction of a system such as a program by constructing a series of increasingly precise abstractions, attempting to verify the system using those abstractions and, if an attempt fails, using a counter-example from the failed attempt to construct a more precise abstraction.

I think the original paper was clarke:cav:2000.

BLAST verifier