@inproceedings{4579,
  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 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.},
  author       = {Beyer, Dirk and Henzinger, Thomas A and Jhala, Ranjit and Majumdar, Ritankar},
  booktitle    = {Proceedings of the 8th international conference, held as part of the joint European Conference on Theory and Practice of Software conference on Fundamental Approaches to Software Engineering},
  isbn         = {9783540254201},
  location     = {Edinburgh, United Kingdom},
  pages        = {2 -- 18},
  publisher    = {Springer Nature},
  title        = {{Checking memory safety with BLAST}},
  doi          = {10.1007/978-3-540-31984-9_2},
  volume       = {3442},
  year         = {2005},
}