---
_id: '2447'
abstract:
- lang: eng
  text: "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"
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ruzica
  full_name: Piskac, Ruzica
  last_name: Piskac
- first_name: Thomas
  full_name: Wies, Thomas
  id: 447BFB88-F248-11E8-B48F-1D18A9856A87
  last_name: Wies
- first_name: Damien
  full_name: Zufferey, Damien
  id: 4397AC76-F248-11E8-B48F-1D18A9856A87
  last_name: Zufferey
  orcid: 0000-0002-3197-8736
citation:
  ama: Piskac R, Wies T, Zufferey D. Automating separation logic using SMT. 2013;8044:773-789.
    doi:<a href="https://doi.org/10.1007/978-3-642-39799-8_54">10.1007/978-3-642-39799-8_54</a>
  apa: 'Piskac, R., Wies, T., &#38; Zufferey, D. (2013). Automating separation logic
    using SMT. Presented at the CAV: Computer Aided Verification, St. Petersburg,
    Russia: Springer. <a href="https://doi.org/10.1007/978-3-642-39799-8_54">https://doi.org/10.1007/978-3-642-39799-8_54</a>'
  chicago: Piskac, Ruzica, Thomas Wies, and Damien Zufferey. “Automating Separation
    Logic Using SMT.” Lecture Notes in Computer Science. Springer, 2013. <a href="https://doi.org/10.1007/978-3-642-39799-8_54">https://doi.org/10.1007/978-3-642-39799-8_54</a>.
  ieee: R. Piskac, T. Wies, and D. Zufferey, “Automating separation logic using SMT,”
    vol. 8044. Springer, pp. 773–789, 2013.
  ista: Piskac R, Wies T, Zufferey D. 2013. Automating separation logic using SMT.
    8044, 773–789.
  mla: Piskac, Ruzica, et al. <i>Automating Separation Logic Using SMT</i>. Vol. 8044,
    Springer, 2013, pp. 773–89, doi:<a href="https://doi.org/10.1007/978-3-642-39799-8_54">10.1007/978-3-642-39799-8_54</a>.
  short: R. Piskac, T. Wies, D. Zufferey, 8044 (2013) 773–789.
conference:
  end_date: 2013-07-19
  location: St. Petersburg, Russia
  name: 'CAV: Computer Aided Verification'
  start_date: 2013-07-13
date_created: 2018-12-11T11:57:43Z
date_published: 2013-07-01T00:00:00Z
date_updated: 2020-08-11T10:09:47Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-39799-8_54
file:
- access_level: open_access
  checksum: 2e866932ab688f47ecd504acb4d5c7d4
  content_type: application/pdf
  creator: dernst
  date_created: 2020-05-15T11:13:01Z
  date_updated: 2020-07-14T12:45:41Z
  file_id: '7859'
  file_name: 2013_CAV_Piskac.pdf
  file_size: 309182
  relation: main_file
file_date_updated: 2020-07-14T12:45:41Z
has_accepted_license: '1'
intvolume: '      8044'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 773 - 789
publication_status: published
publisher: Springer
publist_id: '4456'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Automating separation logic using SMT
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8044
year: '2013'
...