BLAST Publisher's description
from Dirk Beyer
Berkeley Lazy Abstraction Software Verification Tool
BLAST is a software model checker for C programs. The goal of BLAST is to be able to check that software satisfies behavioral properties of the interfaces it uses.
BLAST uses counterexample-driven automatic abstraction refinement to construct an abstract model which is model checked for safety properties. The abstraction is constructed on-the-fly, and only to the required precision.
Give BLAST a try to see what it's all about!
System Requirements:No special requirements.
Program Release Status:
Program Install Support: Install and Uninstall