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
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 version 2.4 (2007-08-29)
- BLAST version 2.3
- BLAST version 2.0
- BLAST version 1.0
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