Software Verification with Blast

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre

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, 2003, pp. 235-239.

Download inofficial, sometimes updated PostScript / PDF document. © 2003 Springer.