BLAST model checker
From Wikipedia, the free encyclopedia
 |
This computing article is a stub. You can help Wikipedia by expanding it. |
The Berkeley Lazy Abstraction Software Verification Tool (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
- Beyer, Dirk; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak (2007). "The Software Model Checker Blast". International Journal on Software Tools for Technology Transfer 9 (5-6): 505–525. doi:10.1007/s10009-007-0044-z.
- Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre (2003). "Software Verification with Blast". In Ball, Thomas; Rajamani, Sriram K.. Proceedings of the 10th SPIN Workshop on Model Checking Software (SPIN 2003). Lecture Notes in Computer Science. 2648. Springer-Verlag. pp. 235–239. ISBN 3-540-40117-2.
