Overview
BLAST (Berkeley Lazy Abstraction Software verification Tool) is a static software verification tool for C language that solves the reachability problem, i.e. whether a given program location can be reached from an entry point (main function) by a valid execution.
Verification of safety properties may be reduced to the reachability, and BLAST is used for such verification in the Linux Driver Verification project.
You may download source code or binary releases of BLAST for Linux on the Files page. The repository checkout instructions are located at the Repository tab. You may file a bug here as well.
BLAST and all the components it relies on are free software. The BLAST itself is released under Apache 2.0 license (see source:LICENSE); for information about the components see source:NOTICE file.
The BLAST has been developed for ten years by a number of people. The version maintained here is based on BLAST v2.5 released in 2008 by Dirk Beyer, Rupak Majumdar, Ranjit Jhala, and Thomas A. Henzinger. For a full list of contributors, refer to the source:README file.
Latest news
BLAST 2.7 has been released
BLAST 2.7 has been released as a result of improvements made within Linux Driver Verification program and for the purpose to take part in Competition on Software Verification at TACAS'12.
BLAST 2.6 has been released
The first final version 2.6 of ISPRAS edition of BLAST has been released. The tool is a development of BLAST 2.5 released in 2008.
Members
Manager: Alexey Khoroshilov, Mikhail Mandrykin, Pavel Shved, Vadim Mutilin
Reporter: Evgeny Novikov, Ilya Shchepetkov, Marina Makienko, Vladimir Gratinskiy