---
res:
  bibo_abstract:
  - 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. @eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Thomas A
      foaf_name: Henzinger, Thomas A
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000−0002−2985−7724
  - foaf_Person:
      foaf_givenName: Ranjit
      foaf_name: Jhala, Ranjit
      foaf_surname: Jhala
  - foaf_Person:
      foaf_givenName: Ritankar
      foaf_name: Majumdar, Ritankar
      foaf_surname: Majumdar
  - foaf_Person:
      foaf_givenName: Grégoire
      foaf_name: Sutre, Grégoire
      foaf_surname: Sutre
  bibo_doi: 10.1007/3-540-44829-2_17
  bibo_volume: 2648
  dct_date: 2003^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/9783540401179
  dct_language: eng
  dct_publisher: Springer@
  dct_title: Software verification with BLAST@
...