1 Introduction
Blast (Berkeley Lazy Abstraction Software verification Tool) is an
automatic verification tool for checking temporal safety properties of
C programs. Given a C program and a temporal safety property, Blast
either statically proves that the program satisfies the safety
property, or provides an execution path that exhibits a violation of
the property (or, since the problem is undecidable, does not
terminate). Blast constructs, explores, and refines abstractions of
the program state space based on lazy predicate abstraction and
interpolation-based predicate discovery. The concepts of Blast are
described in D. Beyer, T.A. Henzinger, Ranjit Jhala, and Rupak
Majumdar, “The Software Model Checker Blast: Applications to Software
Engineering”, Int. Journal on Software Tools for Technology Transfer,
2007.
Online: DOI 10.1007/s10009-007-0044-z.
Blast is relatively independent of the underlying machine and
operating system. However we have only tested it on Intel Pentium
processors under Linux and Microsft Windows with Cygwin. Other
operating systems for the processors above have not been tested, but
the code may work under other operating systems with little work.
Blast is free software, released under the
Modified BSD license.
A PDF version of this document is also available.