BLAST: Berkeley Lazy Abstraction Software Verification Tool

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 first version of BLAST was developed at UC Berkeley by Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre and was supported by the US National Science Foundation.

The BLAST 2.5 Team

Thomas A. Henzinger	Rupak Majumdar
Dirk Beyer	Ranjit Jhala

BLAST Retired --- Replacement Released: CPAchecker

After many years of service, we do not actively maintain BLAST anymore.
However, there are still good news: BLAST got re-implemented in Java, integrating all the lessons we have learned from the BLAST project:
CPAchecker is a re-implementation of BLAST based on the framework of configurable program analysis and supports all essential features of BLAST and much more ...

Check out CPAchecker from: http://cpachecker.sosy-lab.org/

BLAST Documentation

Getting Started

To get started with BLAST:

Download and extract BLAST binaries and examples. To build BLAST from the sources, go to blast/ and run "make".
Add the directory "blast/bin/" to your PATH environment variable.
Go to "blast/test/" and run "./regrtest -block SHORT_REGRESS" to run the (small) examples in "blast/test".
See the Tutorial Introduction section in the BLAST User's Manual to learn how to start with BLAST using the examples in "blast/test".
The model-checking algorithm of BLAST is best explained in Section 2 of our journal paper on BLAST.

BLAST Download

License agreement
The README file

BLAST version 2.5 (2008-07-11)
- blast-2.5_release-notes.txt
- Source distribution blast-2.5.zip
- GNU/Linux binary distributions blast-2.5_linux-bin-x86.zip and blast-2.5_linux-bin-x86_64.tar.gz
- Win32/Cygwin binary distribution (requires cygwin1.dll, cyggmp-3.dll, and KERNEL32.dll) blast-2.5_win32-bin-x86.zip

BLAST version 2.4 (2007-08-29)
- blast-2.4_release-notes.txt
- Source distribution blast-2.4.tar.gz
- GNU/Linux binary distributions blast-2.4_linux-bin-x86.tar.gz and blast-2.4_linux-bin-x86_64.tar.bz2

BLAST version 2.3
- blast-2.3_release-notes.txt
- Source distribution blast-2.3.tar.gz
- GNU/Linux binary distribution blast-2.3_linux_bin.tar.gz

BLAST version 2.0
- blast-2.0.readme.txt
- Source distribution blast-2.0.src.tar.gz
- GNU/Linux binary distribution blast-2.0_linux-bin.tgz
- Eclipse plug-in eclipse-plugin.txt
- Eclipse plug-in eclipse-plugin.zip
- Manual (HTML)
- Manual (PDF)

BLAST version 1.0
- Source distribution blast-1.0.tar.gz
- Windows binary distribution blast-1.2_win-bin.zip (Cygwin)

Experiments

The experiments page provides data on run time of BLAST on several open source programs and properties.
The applications page provides example programs that we have used for checking memory safety and generating test cases.
The lazy shape analysis page provides example programs that we have used for our experiments on lazy shape analysis.

People

BLAST is now developed at several universities.

In Tom Henzinger's group at EPFL.
In Ranjit Jhala's group at UC San Diego.
In Rupak Majumdar's group at UC Los Angeles.
In Dirk Beyer's group at Simon Fraser University.

Many people have contributed to BLAST, including Yvan Bidiville, Adam Chlipala, Jeff Fischer, Ken McMillan, Shaz Qadeer, Andrey Rybalchenko, Gregoire Sutre, Gregory Theoduloz, and Damien Zufferey.

BLAST Papers

The Software Model Checker Blast: Applications to Software Engineering.
Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Int. Journal on Software Tools for Technology Transfer, 9(5-6):505-525, 2007. Invited to special issue of selected papers from FASE 2004/05.

Program Analysis with Dynamic Precision Adjustment.
Dirk Beyer, Thomas A. Henzinger, and Gregory Theoduloz. Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), pages 29-38, IEEE Computer Society Press, 2008.

Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis.
Dirk Beyer, Thomas A. Henzinger, and Gregory Theoduloz. Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007), LNCS 4590, pages 504-518, Springer-Verlag, 2007.

Lazy Shape Analysis
Dirk Beyer, Thomas A. Henzinger, and Gregory Theoduloz. Proceedings of the 18th International Conference on Computer Aided Verification (CAV 2006), LNCS 4144, pages 532-546, Springer-Verlag, 2006.

Checking memory safety with BLAST
Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Proceedings of the 8th International Conference on Fundamental Approaches to Software Engineering (FASE 2005), LNCS 3442, pages 2-18, Springer-Verlag, 2005.

The BLAST query language for software verification
Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Proceedings of the 11th International Static Analysis Symposium (SAS 2004), LNCS 3148, pages 2-18, Springer-Verlag, 2004.

Race checking by context inference
Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Proceedings of the International Conference on Programming Language Design and Implementation (PLDI), ACM Press, 2004.

An Eclipse plug-in for model checking
Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Proceedings of the 12th IEEE International Workshop on Program Comprehension (IWPC 2004), pages 251-255, IEEE Computer Society Press, 2004.

Generating tests from counterexamples
Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Proceedings of the 26th IEEE International Conference on Software Engineering (ICSE 2004), pages 326-335, IEEE Computer Society Press, 2004.

Abstractions from Proofs
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar and Kenneth L. McMillan. In ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages, 2004.

Extreme model checking
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Marco Sanvido. 2003.

Thread-modular Abstraction Refinement
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Shaz Qadeer. Proceedings of the 15th International Conference on Computer-Aided Verification (CAV), LNCS 2725, Springer-Verlag, pages 262-274, 2003.

Software Verification with BLAST
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre. Proceedings of the 10th SPIN Workshop on Model Checking Software (SPIN), LNCS 2648, Springer-Verlag, pages 235-239, 2003.

Temporal-Safety Proofs for Systems Code
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Gregoire Sutre and Westley Weimer. Proceedings of the 14th International Conference on Computer-Aided Verification (CAV), LNCS 2404, Springer-Verlag, pages 526-538, 2002.

Lazy Abstraction
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar and Gregoire Sutre. In ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages, pages 58-70, 2002.

BLAST-related Projects

SLAM - The Software, Languages, Analysis and Model checking project at Microsoft Research.
CIL: An Infrastructure for C Program Analysis and Transformation. - CIL (C Intermediate Language) is a high-level representation along with a set of tools that permit easy analysis and source-to-source transformation of C programs
MAGIC from CMU
ESC/Java - Compaq's Extended Static Checker for Java, a programming tool for finding errors in Java programs.
Meta-level Compilation - A project at Stanford to let programmers build tools that check, optimize, and transform code.

BLAST was part of The Open Source Quality Project (OSQ).

Problems: Contact Dirk Beyer

Update now