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 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.