Checking Memory Safety with Blast

10 years 10 months ago
Checking Memory Safety with Blast
Abstract. 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 rebstractions of the program state space based on lazy predicate ion 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 r...
Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rup
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where FASE
Authors Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
Comments (0)