BLAST

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 BLAST project is supported by the National Science Foundation .

People

Getting Started

To get started with BLAST:

Download and install the Simplify Theorem Prover
Download and extract BLAST binaries and example
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 BLAST using the examples in "../blast/test".

Documentation

Tutoral Slides PPT
Three lectures on Lazy Abstraction Lecture 1 Lecture 2 Lecture 3
Program Verification by Lazy Abstraction, Ranjit Jhala PDF
Demo
BLAST User's Manual PDF

Papers

Interpolant-based Transition Relation Approximation Ranjit Jhala and Kenneth L. McMillan. /Proceedings of the 17th International Conference on Computer-Aided Verification (CAV)/, LNCS 2725, Springer-Verlag, 2005. PDF
Joining Dataflow with Predicates Jeffrey Fischer, Ranjit Jhala and Rupak Majumdar. /Proceedings of FSE 2005. PDF
Path slicing Ranjit Jhala and Rupak Majumdar. /Proceedings of the International Conference on Programming Language Design and Implementation/ (PLDI), ACM Press, 2005. PDF
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. PDF
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. PDF
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. PDF
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. PDF
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. PDF
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. PDF
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. PDF
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. PDF

Related Projects

OSQ Project
SLAM - The Software, Languages, Analysis and Model checking project at Microsoft Research.
MAGIC from CMU
CIL : An Infrastructure for C Program Analysis and Transformation.
ESC/Java: Compaq's Extended Static Checker for Java, a programming tool for finding errors in Java programs.
Meta-level Compilation