BLAST

[ Introduction | Getting Started | Documentation | Related Projects ]

Blast 1.0 has been released!
NEW

Blast's Eclipse plug-in is available now!

Introduction

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 algorithm used by BLAST is described in [HJMS02]. The BLAST project is supported by the National Science Foundation.

People

Thomas A. Henzinger	Ranjit Jhala
Rupak Majumdar	Gregoire Sutre
Dirk Beyer	Adam Chlipala

Getting Started

To get started with BLAST:

Download and install the Simplify Theorem Prover.
Download and extract BLAST binaries and examples. Before venturing further, please read the Copyright agreement.
IMPORTANT The current release is incompatible with Ocaml 3.08. Please use Ocaml 3.07 to compile Blast. We are working on a release to migrate to Ocaml 3.08.1!
Copy the Simplify executable into the "../blast/bin/" directory, and add that directory to your path.
See the Tutorial Introduction section in the BLAST User's Manual to learn how to start with BLAST using the examples in "../blast/test".

Documentation

BLAST User's Manual PDF

[HJMS02]	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.
[HJMNSW02]	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), Lecture Notes in Computer Science 2404, Springer-Verlag, pages 526-538, 2002.
[HJMS03]	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), Lecture Notes in Computer Science 2648, Springer-Verlag, pages 235-239, 2003.
[HJMQ03]	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), Lecture Notes in Computer Science 2725, Springer-Verlag, pages 262-274, 2003.
[HJMQ03]	Extreme model checking Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Marco Sanvido. 2003.
[HJMM04]	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.
[BCHJM04a]	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.
[BHJM04]	An Eclipse plugin 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.
[HJM04]	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.
[BCHJM04b]	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), Lecture Notes in Computer Science 3148, pages 2-18, Springer-Verlag, 2004.

Related Projects

BlAST is one part of The Open Source Quality Project (OSQ).

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.

Last update:
This page is maintained by Rupak Majumdar (rupak@eecs.berkeley.edu)