BLAST model checker
From Wikipedia, the free encyclopedia
The Berkeley Lazy Abstraction Software verification Tool (BLAST) is a software model checking tool for C programs. The task addressed by BLAST is the need to check whether software satisfies the behavioral requirements of its associated interfaces. BLAST employs counterexample-driven automatic abstraction refinement to construct an abstract model that is then model-checked for safety properties. The abstraction is constructed on the fly, and only to the requested precision.
| BLAST | |
|---|---|
| Original authors | Dirk Beyer, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar, Berkeley |
| Developers | Mikhail Mandrykin, Vadim Mutilin, Pavel Shved, Institute for System Programming |
| Stable release | 2.7.3[1]
/ 30 October 2015 |
| Written in | OCaml |
| Operating system | Linux |
| Type | Static code analysis |
| License | Apache License, Version 2.0 |
| Website | forge |
Achievements
BLAST came first in the category DeviceDrivers64 in the 1st Competition on Software Verification (2012) that was held at TACAS 2012 in Tallinn.[2]
BLAST came third (category DeviceDrivers64) in the 2nd Competition on Software Verification (2013) that was held at TACAS 2013 in Rome.[3]
BLAST came first in the category DeviceDrivers64 in the 3rd Competition on Software Verification (2014), that was held at TACAS 2014 in Grenoble.[4]
