Blast is a model checker for C programs based on an algorithm called lazy abstraction. Specifications are given as temporal safety monitors written in C syntax. Blast starts with a very coarse predicate abstraction of the input program and automatically refines the abstraction, on-the-fly and on-demand, until either a bug is found or the specification is proved. Then, Blast provides either an error trace or a succinct proof certificate. Blast has been applied successfully to Linux and Windows device drivers with tens of thousands of lines of C code.
Proceedings of the Tenth International Workshop on Model Checking of Software (SPIN), Lecture Notes in Computer Science 2648, Springer-Verlag, 2003, pp. 235-239.