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/. The BLAST project is supported by the National Science Foundation .


Getting Started

To get started with BLAST:
  1. Download and install the Simplify Theorem Prover
  2. Download and extract BLAST binaries and example
  3. Copy the Simplify executable into the "../blast/bin/" directory, and add that directory to your path,
  4. See the Tutorial Introduction section in the BLAST User's Manual BLAST using the examples in "../blast/test".



Related Projects