A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic

Quang Loc Le; Makoto Tatsuta; Jun Sun; Wei-Ngan Chin

doi:10.1007/978-3-319-63390-9_26

A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic

Quang Loc Le, Makoto Tatsuta, Jun Sun, Wei-Ngan Chin

Research output: Chapter in Book/Report/Conference proceeding › Chapter

187 Downloads (Pure)

Abstract

We consider the satisfiability problem for a fragment of separation logic including inductive predicates with shape and arithmetic properties. We show that the fragment is decidable if the arithmetic properties can be represented as semilinear sets. Our decision procedure is based on a novel algorithm to infer a finite representation for each inductive predicate which precisely characterises its satisfiability. Our analysis shows that the proposed algorithm runs in exponential time in the worst case. We have implemented our decision procedure and integrated it into an existing verification system. Our experiment on benchmarks shows that our procedure helps to verify the benchmarks effectively.

Original language	English
Title of host publication	Computer Aided Verification
Subtitle of host publication	29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II
Publisher	Springer
Volume	10427
ISBN (Electronic)	978-3-319-63390-9
ISBN (Print)	978-3-319-63389-3
DOIs	https://doi.org/10.1007/978-3-319-63390-9_26
Publication status	Published - 24 Jul 2017
Event	29th International Conference on Computer Aided Verification - Heidelberg, Germany Duration: 24 Jul 2017 → 28 Jul 2018

Publication series

Name	Lecture Notes in Computer Science book series
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Name	Theoretical Computer Science and General Issues book sub series
Publisher	Springer
Volume	10427

Conference

Conference	29th International Conference on Computer Aided Verification
Abbreviated title	CAV 2017
Country/Territory	Germany
City	Heidelberg
Period	24/07/17 → 28/07/18

Access to Document

10.1007/978-3-319-63390-9_26

PublicationAccepted author manuscript, 454 KBLicence: CC BY-NC-ND

Cite this

Le, Q. L., Tatsuta, M., Sun, J., & Chin, W.-N. (2017). A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic. In Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II (Vol. 10427). (Lecture Notes in Computer Science book series), ( Theoretical Computer Science and General Issues book sub series; Vol. 10427). Springer. https://doi.org/10.1007/978-3-319-63390-9_26

Le, Quang Loc ; Tatsuta, Makoto ; Sun, Jun et al. / A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic. Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II. Vol. 10427 Springer, 2017. (Lecture Notes in Computer Science book series). ( Theoretical Computer Science and General Issues book sub series).

@inbook{dfe927c2788f40bea6615727829673a0,

title = "A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic",

abstract = "We consider the satisfiability problem for a fragment of separation logic including inductive predicates with shape and arithmetic properties. We show that the fragment is decidable if the arithmetic properties can be represented as semilinear sets. Our decision procedure is based on a novel algorithm to infer a finite representation for each inductive predicate which precisely characterises its satisfiability. Our analysis shows that the proposed algorithm runs in exponential time in the worst case. We have implemented our decision procedure and integrated it into an existing verification system. Our experiment on benchmarks shows that our procedure helps to verify the benchmarks effectively.",

author = "Le, {Quang Loc} and Makoto Tatsuta and Jun Sun and Wei-Ngan Chin",

year = "2017",

month = jul,

day = "24",

doi = "10.1007/978-3-319-63390-9_26",

language = "English",

isbn = "978-3-319-63389-3",

volume = "10427",

series = "Lecture Notes in Computer Science book series",

publisher = "Springer",

booktitle = "Computer Aided Verification",

note = "29th International Conference on Computer Aided Verification, CAV 2017 ; Conference date: 24-07-2017 Through 28-07-2018",

}

Le, QL, Tatsuta, M, Sun, J & Chin, W-N 2017, A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic. in Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II. vol. 10427, Lecture Notes in Computer Science book series, Theoretical Computer Science and General Issues book sub series, vol. 10427, Springer, 29th International Conference on Computer Aided Verification, Heidelberg, Germany, 24/07/17. https://doi.org/10.1007/978-3-319-63390-9_26

A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic. / Le, Quang Loc; Tatsuta, Makoto; Sun, Jun et al.
Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II. Vol. 10427 Springer, 2017. (Lecture Notes in Computer Science book series), ( Theoretical Computer Science and General Issues book sub series; Vol. 10427).

Research output: Chapter in Book/Report/Conference proceeding › Chapter

TY - CHAP

T1 - A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic

AU - Le, Quang Loc

AU - Tatsuta, Makoto

AU - Sun, Jun

AU - Chin, Wei-Ngan

PY - 2017/7/24

Y1 - 2017/7/24

N2 - We consider the satisfiability problem for a fragment of separation logic including inductive predicates with shape and arithmetic properties. We show that the fragment is decidable if the arithmetic properties can be represented as semilinear sets. Our decision procedure is based on a novel algorithm to infer a finite representation for each inductive predicate which precisely characterises its satisfiability. Our analysis shows that the proposed algorithm runs in exponential time in the worst case. We have implemented our decision procedure and integrated it into an existing verification system. Our experiment on benchmarks shows that our procedure helps to verify the benchmarks effectively.

AB - We consider the satisfiability problem for a fragment of separation logic including inductive predicates with shape and arithmetic properties. We show that the fragment is decidable if the arithmetic properties can be represented as semilinear sets. Our decision procedure is based on a novel algorithm to infer a finite representation for each inductive predicate which precisely characterises its satisfiability. Our analysis shows that the proposed algorithm runs in exponential time in the worst case. We have implemented our decision procedure and integrated it into an existing verification system. Our experiment on benchmarks shows that our procedure helps to verify the benchmarks effectively.

U2 - 10.1007/978-3-319-63390-9_26

DO - 10.1007/978-3-319-63390-9_26

M3 - Chapter

SN - 978-3-319-63389-3

VL - 10427

T3 - Lecture Notes in Computer Science book series

BT - Computer Aided Verification

PB - Springer

T2 - 29th International Conference on Computer Aided Verification

Y2 - 24 July 2017 through 28 July 2018

ER -

Le QL, Tatsuta M, Sun J, Chin WN. A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic. In Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II. Vol. 10427. Springer. 2017. (Lecture Notes in Computer Science book series). ( Theoretical Computer Science and General Issues book sub series). doi: 10.1007/978-3-319-63390-9_26

A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this