Paper Accepted at CAV 2017

Our group has had a paper accepted at the 29th International Conference on Computer Aided Verification (CAV 2017) about our work on decidable fragments of separation logic. A PDF postprint is available online now:

  • Q. L. Le, T. Makoto, J. Sun, and W. Chin. A decidable fragment in separation logic with inductive predicates and arithmetic. In Proc. International Conference on Computer Aided Verification (CAV 2017), LNCS, Springer, 2017.
    [PDF] [Bibtex]
    @inproceedings{Le-Makoto-Sun-Chin17a,
    author = {Quang Loc Le and Tatsuta Makoto and Jun Sun and Wei-Ngan Chin},
    title = {A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic},
    booktitle = {{Proc. International Conference on Computer Aided Verification (CAV 2017)}},
    year = {2017},
    series = {LNCS},
    publisher = {Springer},
    note = {To appear},
    pdf = {http://sav.sutd.edu.sg/wp-content/uploads/2016/08/cav2017.pdf},
    }

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.