---
_id: '4467'
abstract:
- lang: eng
  text: 'BLAST (the Berkeley Lazy Abstraction Software verification Tool) is a verification
    system for checking safety properties of C programs using automatic property-driven
    construction and model checking of software abstractions. Blast implements an
    abstract-model check-refine loop to check for reachability of a specified label
    in the program. The abstract model is built on the fly using predicate abstraction.
    This model is then checked for reachability. If there is no (abstract) path to
    the specified error label, Blast reports that the system is safe and produces
    a succinct proof. Otherwise, it checks if the path is feasible using symbolic
    execution of the program. If the path is feasible, Blast outputs the path as an
    error trace, otherwise, it uses the infeasibility of the path to refine the abstract
    model. Blast short-circuits the loop from abstraction to verification to refinement,
    integrating the three steps tightly through “lazy abstraction” [5]. This integration
    can offer significant advantages in performance by avoiding the repetition of
    work from one iteration of the loop to the next. '
acknowledgement: This work was supported in part by the NSF grants CCR-0085949 and
  CCR-9988172, the DARPA PCES grant F33615-00-C-1693, the MARCO GSRC grant 98-DT-660,
  and a Microsoft Research Fellowship.
alternative_title:
- LNCS
article_processing_charge: No
author:
- 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
- first_name: Grégoire
  full_name: Sutre, Grégoire
  last_name: Sutre
citation:
  ama: 'Henzinger TA, Jhala R, Majumdar R, Sutre G. Software verification with BLAST.
    In: <i>Proceedings of the 10th International SPIN Workshop </i>. Vol 2648. Springer;
    2003:235-239. doi:<a href="https://doi.org/10.1007/3-540-44829-2_17">10.1007/3-540-44829-2_17</a>'
  apa: 'Henzinger, T. A., Jhala, R., Majumdar, R., &#38; Sutre, G. (2003). Software
    verification with BLAST. In <i>Proceedings of the 10th International SPIN Workshop
    </i> (Vol. 2648, pp. 235–239). Portland, OR, USA: Springer. <a href="https://doi.org/10.1007/3-540-44829-2_17">https://doi.org/10.1007/3-540-44829-2_17</a>'
  chicago: Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Grégoire Sutre.
    “Software Verification with BLAST.” In <i>Proceedings of the 10th International
    SPIN Workshop </i>, 2648:235–39. Springer, 2003. <a href="https://doi.org/10.1007/3-540-44829-2_17">https://doi.org/10.1007/3-540-44829-2_17</a>.
  ieee: T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, “Software verification
    with BLAST,” in <i>Proceedings of the 10th International SPIN Workshop </i>, Portland,
    OR, USA, 2003, vol. 2648, pp. 235–239.
  ista: 'Henzinger TA, Jhala R, Majumdar R, Sutre G. 2003. Software verification with
    BLAST. Proceedings of the 10th International SPIN Workshop . SPIN: Model Checking
    Software, LNCS, vol. 2648, 235–239.'
  mla: Henzinger, Thomas A., et al. “Software Verification with BLAST.” <i>Proceedings
    of the 10th International SPIN Workshop </i>, vol. 2648, Springer, 2003, pp. 235–39,
    doi:<a href="https://doi.org/10.1007/3-540-44829-2_17">10.1007/3-540-44829-2_17</a>.
  short: T.A. Henzinger, R. Jhala, R. Majumdar, G. Sutre, in:, Proceedings of the
    10th International SPIN Workshop , Springer, 2003, pp. 235–239.
conference:
  end_date: 2003-05-10
  location: Portland, OR, USA
  name: 'SPIN: Model Checking Software'
  start_date: 2003-05-09
date_created: 2018-12-11T12:09:00Z
date_published: 2003-04-28T00:00:00Z
date_updated: 2024-01-08T14:05:29Z
day: '28'
doi: 10.1007/3-540-44829-2_17
extern: '1'
intvolume: '      2648'
language:
- iso: eng
month: '04'
oa_version: None
page: 235 - 239
publication: 'Proceedings of the 10th International SPIN Workshop '
publication_identifier:
  isbn:
  - '9783540401179'
publication_status: published
publisher: Springer
publist_id: '264'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Software verification with BLAST
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2648
year: '2003'
...