---
res:
  bibo_abstract:
  - "Separation logic (SL) has gained widespread popularity because of its ability
    to succinctly express complex invariants of a program’s heap configurations. Several
    specialized provers have been developed for decidable SL fragments. However, these
    provers cannot be easily extended or combined with solvers for other theories
    that are important in program verification, e.g., linear arithmetic. In this paper,
    we present a reduction of decidable SL fragments to a decidable first-order theory
    that fits well into the satisfiability modulo theories (SMT) framework. We show
    how to use this reduction to automate satisfiability, entailment, frame inference,
    and abduction problems for separation logic using SMT solvers. Our approach provides
    a simple method of integrating separation logic into existing verification tools
    that provide SMT backends, and an elegant way of combining SL fragments with other
    decidable first-order theories. We implemented this approach in a verification
    tool and applied it to heap-manipulating programs whose verification involves
    reasoning in theory combinations.\r\n@eng"
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Ruzica
      foaf_name: Piskac, Ruzica
      foaf_surname: Piskac
  - foaf_Person:
      foaf_givenName: Thomas
      foaf_name: Wies, Thomas
      foaf_surname: Wies
      foaf_workInfoHomepage: http://www.librecat.org/personId=447BFB88-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Damien
      foaf_name: Zufferey, Damien
      foaf_surname: Zufferey
      foaf_workInfoHomepage: http://www.librecat.org/personId=4397AC76-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-3197-8736
  bibo_doi: 10.1007/978-3-642-39799-8_54
  bibo_volume: 8044
  dct_date: 2013^xs_gYear
  dct_language: eng
  dct_publisher: Springer@
  dct_title: Automating separation logic using SMT@
...