Model checking for symbolic-heap separation logic with inductive predicates

Brotherston, James and Gorogiannis, Nikos and Kanovich, Max and Rowe, Reuben (2016) Model checking for symbolic-heap separation logic with inductive predicates. In: 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL '16, January 20-22, 2016, St Petersburg, FL, USA. (doi:https://doi.org/10.1145/2914770.2837621) (Full text available)

PDF - Publisher pdf
Download (339kB) Preview
[img]
Preview
Official URL
http://doi.org/10.1145/2914770.2837621

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.

Item Type: Conference or workshop item (Paper)
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Reuben Rowe
Date Deposited: 06 Dec 2016 12:14 UTC
Last Modified: 08 Dec 2016 10:35 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/59465 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year