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.

Patch Descriptions

Use system libraries and applications instead of building them from sources distributed with BLAST.
Make CVC3 be the default SMT solver, since it is the only one supported by BLAST that is currently available from Fedora (and indeed, is the only freely redistributable one, as far as I can tell).
Fix a few escape characters in regular expressions; some are missing and some are extraneous.

Back to the RPMS

Last modified: Tue Nov 15 20:49:27 MST 2011 by Jerry James