Synergy

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 comparing the 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.


References

  1. The Synergy of Precise and Fast Abstractions for Program Verification, Sharygina, N.; Tonetta, S.; Tsitovich, A. , 24th Annual ACM Symposium on Applied Computing (SAC), Honolulu, USA, p.566-573, ACM (2009)