---
OA_type: closed access
_id: '4579'
abstract:
- lang: eng
  text: 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.
acknowledgement: This research was supported in part by the NSF grants CCR-0234690,
  CCR-0225610, and ITR-0326577.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Dirk
  full_name: Beyer, Dirk
  last_name: Beyer
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Ranjit
  full_name: Jhala, Ranjit
  last_name: Jhala
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
citation:
  ama: 'Beyer D, Henzinger TA, Jhala R, Majumdar R. Checking memory safety with BLAST.
    In: <i>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</i>. Vol 3442. Springer Nature; 2005:2-18.
    doi:<a href="https://doi.org/10.1007/978-3-540-31984-9_2">10.1007/978-3-540-31984-9_2</a>'
  apa: 'Beyer, D., Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2005). Checking
    memory safety with BLAST. In <i>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</i> (Vol. 3442, pp.
    2–18). Edinburgh, United Kingdom: Springer Nature. <a href="https://doi.org/10.1007/978-3-540-31984-9_2">https://doi.org/10.1007/978-3-540-31984-9_2</a>'
  chicago: Beyer, Dirk, Thomas A Henzinger, Ranjit Jhala, and Ritankar Majumdar. “Checking
    Memory Safety with BLAST.” In <i>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</i>, 3442:2–18. Springer
    Nature, 2005. <a href="https://doi.org/10.1007/978-3-540-31984-9_2">https://doi.org/10.1007/978-3-540-31984-9_2</a>.
  ieee: D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar, “Checking memory safety
    with BLAST,” in <i>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</i>, Edinburgh, United Kingdom,
    2005, vol. 3442, pp. 2–18.
  ista: 'Beyer D, Henzinger TA, Jhala R, Majumdar R. 2005. Checking memory safety
    with BLAST. 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. FASE: Fundamental Approaches To Software Engineering,
    LNCS, vol. 3442, 2–18.'
  mla: Beyer, Dirk, et al. “Checking Memory Safety with BLAST.” <i>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</i>, vol. 3442, Springer Nature, 2005, pp. 2–18, doi:<a href="https://doi.org/10.1007/978-3-540-31984-9_2">10.1007/978-3-540-31984-9_2</a>.
  short: D. Beyer, T.A. Henzinger, R. Jhala, R. Majumdar, in:, 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, Springer Nature, 2005, pp. 2–18.
conference:
  end_date: 2005-04-08
  location: Edinburgh, United Kingdom
  name: 'FASE: Fundamental Approaches To Software Engineering'
  start_date: 2005-04-04
date_created: 2018-12-11T12:09:34Z
date_published: 2005-03-24T00:00:00Z
date_updated: 2026-09-30T14:10:19Z
day: '24'
doi: 10.1007/978-3-540-31984-9_2
extern: '1'
fulldoi: https://doi.org/10.1007/978-3-540-31984-9_2
intvolume: '      3442'
language:
- iso: eng
month: '03'
oa_version: None
page: 2 - 18
publication: 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
publication_identifier:
  isbn:
  - '9783540254201'
publication_status: published
publisher: Springer Nature
publist_id: '131'
status: public
title: Checking memory safety with BLAST
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 3442
year: '2005'
...