Automating separation logic using SMT

Ruzica Piskac, Thomas Wies, Damien Zufferey

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 25th International Conference, CAV 2013, Proceedings
Pages773-789
Number of pages17
Volume8044 LNCS
DOIs
StatePublished - 2013
Event25th International Conference on Computer Aided Verification, CAV 2013 - Saint Petersburg, Russian Federation
Duration: Jul 13 2013Jul 19 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8044 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other25th International Conference on Computer Aided Verification, CAV 2013
CountryRussian Federation
CitySaint Petersburg
Period7/13/137/19/13

Fingerprint

Separation Logic
Modulo
Program Verification
Fragment
Heap
First-order
Abduction
Express
Reasoning
Configuration
Invariant

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Piskac, R., Wies, T., & Zufferey, D. (2013). Automating separation logic using SMT. In Computer Aided Verification - 25th International Conference, CAV 2013, Proceedings (Vol. 8044 LNCS, pp. 773-789). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8044 LNCS). https://doi.org/10.1007/978-3-642-39799-8_54

Automating separation logic using SMT. / Piskac, Ruzica; Wies, Thomas; Zufferey, Damien.

Computer Aided Verification - 25th International Conference, CAV 2013, Proceedings. Vol. 8044 LNCS 2013. p. 773-789 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8044 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Piskac, R, Wies, T & Zufferey, D 2013, Automating separation logic using SMT. in Computer Aided Verification - 25th International Conference, CAV 2013, Proceedings. vol. 8044 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8044 LNCS, pp. 773-789, 25th International Conference on Computer Aided Verification, CAV 2013, Saint Petersburg, Russian Federation, 7/13/13. https://doi.org/10.1007/978-3-642-39799-8_54
Piskac R, Wies T, Zufferey D. Automating separation logic using SMT. In Computer Aided Verification - 25th International Conference, CAV 2013, Proceedings. Vol. 8044 LNCS. 2013. p. 773-789. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-39799-8_54
Piskac, Ruzica ; Wies, Thomas ; Zufferey, Damien. / Automating separation logic using SMT. Computer Aided Verification - 25th International Conference, CAV 2013, Proceedings. Vol. 8044 LNCS 2013. pp. 773-789 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{2d89789d9b6b458a9f301dd2188a9168,
title = "Automating separation logic using SMT",
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.",
author = "Ruzica Piskac and Thomas Wies and Damien Zufferey",
year = "2013",
doi = "10.1007/978-3-642-39799-8_54",
language = "English (US)",
isbn = "9783642397981",
volume = "8044 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "773--789",
booktitle = "Computer Aided Verification - 25th International Conference, CAV 2013, Proceedings",

}

TY - GEN

T1 - Automating separation logic using SMT

AU - Piskac, Ruzica

AU - Wies, Thomas

AU - Zufferey, Damien

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84881179310&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84881179310&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-39799-8_54

DO - 10.1007/978-3-642-39799-8_54

M3 - Conference contribution

SN - 9783642397981

VL - 8044 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 773

EP - 789

BT - Computer Aided Verification - 25th International Conference, CAV 2013, Proceedings

ER -