14-Oct-2011: BLAST 2.7 released

Submitted by admin on Mon, 23/01/2012 - 08:22

Linux Verification Center announces the release of BLAST 2.7 - a new version of an open source model checker for C programs. The tool automatically checks if a C program satisfies behavioral properties of the interfaces it uses. BLAST is based on counterexample-driven automatic abstraction refinement to construct an abstract model which is model checked for safety properties.

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.0 Team includes Thomas A. Henzinger, Dirk Beyer, Rupak Majumdar, and Ranjit Jhala. The latest release of the team is BLAST 2.5 of 2008.

BLAST 2.7 is a result of improvements made in BLAST 2.6 by Linux Verification Center team within Linux Driver Verification program and for the purpose to take part in Competition on Software Verification at TACAS'12.

The main improvements are as follows.

  • Analysis speedup
    • Fast and sound algorithm for alias analysis for pointers to
      structures without dereference depth limit enforced. Does not

      terminate on some programs with arbitrary-depth lists.

    • Add some normalization for better caching of postcondition requests.
    • Improved performance of lattice states merge.
  • New features
    • Re-animated function pointer support (-fp), which, however, doesn't

      distpatch correctly two or more functions aliased by the pointer.

    • Updated 64- and 32-bit versions of CSIsat allow you to analyze
      programs with as large numbers as your architecture supports.
  • Infrastructure improvements
    • Separated supported and unsupported options. Most recently added

      options has been made default.

    • Regression test suite may work in "competition" mode.
  • Bug fixes
    • Formulae caching in O(logN) useful blocks algorithm fixed (less
      FOCIinterface.SAT exceptions).

Sources and binaries are available from the Files page of the project at ISPRAS forge. See also the original project page.