Decision procedure for separation logic with inductive predicates and Presburger arithmetic

Makoto Tatsuta, Quang Loc Le, Wei-Ngan Chin

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

    156 Downloads (Pure)


    This paper considers the satisfiability problem of symbolic heaps in separation logic with Presburger arithmetic and inductive definitions. First the system without any restrictions is proved to be undecidable. Secondly this paper proposes some syntactic restrictions for decidability. These restrictions are identified based on a new decidable subsystem of Presburger arithmetic with inductive definitions. In the subsystem of arithmetic, every inductively defined predicate represents an eventually periodic set and can be eliminated. The proposed system is quite general as it can handle the satisfiability of the arithmetical parts of fairly complex predicates such as sorted lists and AVL trees. Finally, we prove the decidability by presenting a decision procedure for symbolic heaps with the restricted inductive definitions and arithmetic.
    Original languageEnglish
    Title of host publicationProgramming Languages and Systems.
    Subtitle of host publication14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21 - 23, 2016, Proceedings
    ISBN (Electronic)978-3-319-47958-3
    Publication statusPublished - 9 Oct 2016
    Event14th Asian Symposium on Programming Languages and Systems: APLAS 2016 - Hanoi, Viet Nam
    Duration: 21 Nov 201623 Nov 2016

    Publication series

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


    Conference14th Asian Symposium on Programming Languages and Systems
    Country/TerritoryViet Nam


    Dive into the research topics of 'Decision procedure for separation logic with inductive predicates and Presburger arithmetic'. Together they form a unique fingerprint.

    Cite this