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 proceedingChapter

147 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 languageEnglish
Title of host publication Computer Aided Verification
Subtitle of host publication29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II
PublisherSpringer
Volume10427
ISBN (Electronic)978-3-319-63390-9
ISBN (Print)978-3-319-63389-3
DOIs
Publication statusPublished - 24 Jul 2017
Event29th International Conference on Computer Aided Verification - Heidelberg, Germany
Duration: 24 Jul 201728 Jul 2018

Publication series

NameLecture Notes in Computer Science book series
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349
Name Theoretical Computer Science and General Issues book sub series
PublisherSpringer
Volume10427

Conference

Conference29th International Conference on Computer Aided Verification
Abbreviated titleCAV 2017
CountryGermany
CityHeidelberg
Period24/07/1728/07/18

Fingerprint Dive into the research topics of 'A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic'. Together they form a unique fingerprint.

  • 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