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
Volume8559 LNCS
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)03029743
ISSN (Electronic)16113349

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

Fingerprint

Separation Logic
Decision Procedures
Reasoning
Data structures
Data Structures
Heap
Classical Logic
Correctness
Fragment
First-order Logic
Complex Structure
Heuristics
Logic
Verify
First-order

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

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 (Vol. 8559 LNCS, 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

Automating separation logic with trees and data. / Piskac, Ruzica; Wies, Thomas; Zufferey, Damien.

Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Vol. 8559 LNCS Springer Verlag, 2014. p. 711-728 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8559 LNCS).

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

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. vol. 8559 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8559 LNCS, Springer Verlag, pp. 711-728, 26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, 7/18/14. https://doi.org/10.1007/978-3-319-08867-9_47
Piskac R, Wies T, Zufferey D. 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. Vol. 8559 LNCS. Springer Verlag. 2014. p. 711-728. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-08867-9_47
Piskac, Ruzica ; Wies, Thomas ; Zufferey, Damien. / Automating separation logic with trees and data. Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Vol. 8559 LNCS Springer Verlag, 2014. pp. 711-728 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{63e60f8104894578a63a4cb8aef17ad4,
title = "Automating separation logic with trees and data",
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.",
author = "Ruzica Piskac and Thomas Wies and Damien Zufferey",
year = "2014",
doi = "10.1007/978-3-319-08867-9_47",
language = "English (US)",
isbn = "9783319088662",
volume = "8559 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "711--728",
booktitle = "Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings",

}

TY - GEN

T1 - Automating separation logic with trees and data

AU - Piskac, Ruzica

AU - Wies, Thomas

AU - Zufferey, Damien

PY - 2014

Y1 - 2014

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

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

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

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

U2 - 10.1007/978-3-319-08867-9_47

DO - 10.1007/978-3-319-08867-9_47

M3 - Conference contribution

AN - SCOPUS:84904805039

SN - 9783319088662

VL - 8559 LNCS

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

SP - 711

EP - 728

BT - Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings

PB - Springer Verlag

ER -