The techniques developed for "The Synergy of Precise and Fast Abstractions for Program Verification" project are implemented on top of SATABS model-checker for ANSI-C programs. The tool allows to compare effectiveness of abstraction techniques in CEGAR-based verification. Details of the techniques can be found in [1].
Tool binary (1,6MB) compiled for Linux/i386.