Automating separation logic with trees and data

Ruzica Piskac, Thomas Wies, Damien Zufferey

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

Abstract

Separation logic (SL) is a widely used formalism for verifying heap manipulating programs. Existing SL solvers focus on decidable fragments for list-like structures. More complex data structures such as trees are typically unsupported in implementations, or handled by incomplete heuristics. While complete decision procedures for reasoning about trees have been proposed, these procedures suffer from high complexity, or make global assumptions about the heap that contradict the separation logic philosophy of local reasoning. In this paper, we present a fragment of classical first-order logic for local reasoning about tree-like data structures. The logic is decidable in NP and the decision procedure allows for combinations with other decidable first-order theories for reasoning about data. Such extensions are essential for proving functional correctness properties. We have implemented our decision procedure and, building on earlier work on translating SL proof obligations into classical logic, integrated it into an SL-based verification tool. We successfully used the tool to verify functional correctness of tree-based data structure implementations.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
PublisherSpringer Verlag
Pages711-728
Number of pages18
ISBN (Print)9783319088662
DOIs
StatePublished - 2014
Event26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Austria
Duration: Jul 18 2014Jul 22 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8559 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014
CountryAustria
CityVienna
Period7/18/147/22/14

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Automating separation logic with trees and data'. Together they form a unique fingerprint.

  • Cite this

    Piskac, R., Wies, T., & Zufferey, D. (2014). Automating separation logic with trees and data. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings (pp. 711-728). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8559 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-08867-9_47