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.
Note: It appears that this package cannot be submitted to Fedora, because it includes modified code from the Vampyre prover, which has a non-free license. In particular, its license is BSD, but includes a "for research purposes only" clause. If the authors can be persuaded to remove that clause, we could get Blast into Fedora.
For the purpose of submitting this package to Fedora, here is the RPM spec file.