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.
| Attributes | Values |
|---|---|
| rdfs:comment |
|
| foaf:name |
|
| foaf:homepage | |
| author | |
| developer | |
| genre | |
| latest release date |
|
| latest release version |
|
| license | |
| operating system | |
| programming language |