Model checking for symbolic-heap separation logic with inductive predicates. / Brotherston, James; Gorogiannis, Nikos; Kanovich, Max; Rowe, Reuben.

POPL '16 Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 2016. p. 84-96.

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

Published

Documents

  • James Brotherston
  • Nikos Gorogiannis
  • Max Kanovich
  • Reuben Rowe

Abstract

We investigate the model checking problem for symbolic-heap separation logic with user-defined inductive predicates, i.e., the problem of checking that a given stack-heap memory state satisfies a given formula in this language, as arises e.g. in software testing or runtime verification. First, we show that the problem is *decidable*; specifically, we present a bottom-up fixed point algorithm that decides the problem and runs in exponential time in the size of the problem instance. Second, we show that, while model checking for the full language is EXPTIME-complete, the problem becomes NP-complete or PTIME-solvable when we impose natural syntactic restrictions on the schemata defining the inductive predicates. We additionally present NP and PTIME algorithms for these restricted fragments. Finally, we report on the experimental performance of our procedures on a variety of specifications extracted from programs, exercising multiple combinations of syntactic restrictions.
Original languageEnglish
Title of host publicationPOPL '16 Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
PublisherACM
Pages84-96
Number of pages13
ISBN (Print)978-1-4503-3549-2
DOIs
Publication statusPublished - 11 Jan 2016
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 34708602