BLAST model checker
From Wikipedia, the free encyclopedia
BLAST is a software model-checking tool for C programs. The task addressed by BLAST is the need to check whether software satisfies the behavioral requirements of its associated interfaces. BLAST employs counterexample-driven automatic abstraction refinement to construct an abstract model that is then model-checked for safety properties. The abstraction is constructed on the fly, and only to the requested precision.
[edit] References
- Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre. Software Verification with Blast. In Proceedings of the 10th SPIN Workshop on Model Checking Software (SPIN 2003), LNCS 2648, Springer-Verlag, pages 235–239, 2003.
