OVERVIEW: 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. BLAST is relatively independent of the underlying machine and operating system. However we have only tested it under Intel Pentium processors under Linux and Microsft Windows under 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. DOCUMENTATION: The BLAST manual is distributed in HTML, PDF, and Postscript files. See doc/blast.{ps,pdf,html} It is also available on the World Wide Web, at http://mtc.epfl.ch/blast/ AVAILABILITY: The complete BLAST distribution can be downloaded from http://mtc.epfl.ch/blast/ AUTHORS: The current version of BLAST was developed and is maintained by Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Many people have contributed to BLAST, including Adam Chlipala, Jeff Fischer, Ken McMillan, Shaz Qadeer, Gregoire Sutre, Gregory Theoduloz, and Damien Zufferey. BUG REPORTS AND USER FEEDBACK: Send your bug reports by E-mail to: Dirk Beyer: firstname.lastname@sfu.ca or Rupak Majumdar: firstname@cs.ucla.edu or Ranjit Jhala: lastname@cs.ucla.edu To be effective, bug reports should include a complete program (preferably small) that exhibits the unexpected behavior, and the configuration you are using (machine type, OCaml version, etc). CONTENTS: BLAST package: blast/README this file blast/COPYRIGHT.txt license (BSD) blast/Makefile main Makefile blast/config.make Makefile configurations blast/rules.make rules used by the Makefile blast/bldutils/ build utilities (cruise control) blast/doc/ documentation, manual, api reference blast/focibin/ the FOCI interpolation procedure blast/include/ various cmi files to be included during the build blast/lib/ library files used by the linker blast/psrc/ the files for the model checker BLAST blast/simplify/ the Simplify Theorem Prover blast/spec/ the files for the BLAST specification language blast/test/ simple test cases blast/vampyre/ the Vampyre Proof Generating Theorem Prover Other (third party) packages: caddie/ Ocaml wrappers for CuDD BDD library cil_1_3_1/ the CIL infrastructure for C programs cudd/ the Colorado University Decision Diagram package utils utility files INSTALLATION: In the main directory for BLAST, do the following: make distclean make