Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar
Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, Blast statically proves that either the program satisfies the safety property or the program has an execution trace that exhibits a violation of the property. Blast constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. We show how Blast can be used to statically prove memory safety for C programs. We take a two-step approach. First, we use CCured, a type-based memory safety analyzer, to annotate with run-time checks all program points that cannot be proved memory safe by the type system. Second, we use Blast to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate for the remaining run-time checks execution traces that witness them fail. Our experience shows that Blast can remove many of the run-time checks added by CCured and provide useful information to the programmer about many of the remaining checks.
Proceedings of the International Conference on Fundamental Approaches to Software Engineering (FASE), Lecture Notes in Computer Science 3442, Springer, 2005, pp. 2-18.