A decidable fragment in separation logic with inductive predicates and arithmetic

• Main Authors: LE, Quang Loc, TATSUTA, Makoto, SUN, Jun, CHIN, Wei-Ngan
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2017
• Subjects: Decidability; Inductive predicates; Satisfiability solving; Separation logic; Software Engineering; Theory and Algorithms
• Online Access: https://ink.library.smu.edu.sg/sis_research/4702; https://ink.library.smu.edu.sg/context/sis_research/article/5705/viewcontent/Decidable_fragment_cav2017_av.pdf
• Institution: Singapore Management University

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