16-Sep-2011: BLAST 2.6 released

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

Linux Verification Center announces the release of BLAST 2.6 - 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.6 is a result of improvements made in BLAST 2.5 by Linux Verification Center team within Linux Driver Verification program.

The main improvements are as follows.

  • Analysis speedup
    • Speedup ranges from 8 times on small-sized programs to 30 times on medium-sized programs
    • Logarithmic algorithm for useful-blocks (significantly speedup of trace analysis)
    • Improved integration with SMT solvers
      • efficient string concatenation
      • caching of converted formulae
      • optimization of CVC3 options for BLAST use cases
    • Formulae normalization has been moved to solvers since solvers do it faster (option -skipnorm)
    • Alias analysis speedup
      • must-aliases are handled separately and faster than may-aliases (option -nomusts)
      • removed unnecessary debug prints from alias iteration (even a check for debug flag impacts performance significantly in hot places)
    • BLAST-specific tuning of OCaml virtual machine options (script "ocamltune")
  • Important bug fixes
    • Fixed unsound analysis when lattices are used (options -stop-sep and -merge) (Time of analysis has been increased by a factor of 1.5, but the inherent imprecision in lattices no longer makes BLAST miss bugs). See bug #330
    • bool-to-int casting in function calls fixed. See bug #334
  • Frontend
    • C frontend (CIL) uplift, fixes and workarounds (see -ignoredupfn and -nosserr options)
    • Some errors have been made warnings
  • New features
    • constrain stack depth to be analyzed; see options -fdepth, -important-attrs, and -inline-attrs
    • treat constant pointers as must aliases (see option -const)
  • Infrastructure improvements

    • Regression test suite improved

    • Got rid of non-free software (Simplify solver was replaced by CVC3, ditched unused Vampyre, FOCI, and CLPprover)

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