---
res:
  bibo_abstract:
  - Many software model checkers are based on predicate abstraction. If the verification
    goal depends on pointer structures, the approach does not work well, because it
    is difficult to find adequate predicate abstractions for the heap. In contrast,
    shape analysis, which uses graph-based heap abstractions, can provide a compact
    representation of recursive data structures. We integrate shape analysis into
    the software model checker Blast. Because shape analysis is expensive, we do not
    apply it globally. Instead, we ensure that, like predicates, shape graphs are
    computed and stored locally, only where necessary for proving the verification
    goal. To achieve this, we extend lazy abstraction refinement, which so far has
    been used only for predicate abstractions, to three-valued logical structures.
    This approach does not only increase the precision of model checking, but it also
    increases the efficiency of shape analysis. We implemented the technique by extending
    Blast with calls to Tvla.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Dirk
      foaf_name: Beyer, Dirk
      foaf_surname: Beyer
  - 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: Grégory
      foaf_name: Théoduloz, Grégory
      foaf_surname: Théoduloz
  bibo_doi: 10.1007/11817963_48
  bibo_volume: 4144
  dct_date: 2006^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/9783540374060
  dct_language: eng
  dct_publisher: Springer@
  dct_title: Lazy shape analysis@
...