UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Model checking for symbolic-heap separation logic with inductive predicates

Brotherston, J; Gorogiannis, N; Kanovich, MI; Rowe, R; (2016) Model checking for symbolic-heap separation logic with inductive predicates. In: Bodik, R and Majumdar, R, (eds.) (pp. pp. 84-96). ACM Green open access

[img]
Preview
Text
p84-brotherston.pdf - Published version

Download (485kB) | Preview

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.

Type: Proceedings paper
Title: Model checking for symbolic-heap separation logic with inductive predicates
ISBN-13: 978-1-4503-3549-2
Open access status: An open access version is available from UCL Discovery
DOI: 10.1145/2837614.2837621
Publisher version: http://dl.acm.org/citation.cfm?id=2837614
Language: English
Additional information: Open Access. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s). Copyright is held by the author/owner(s).
UCL classification: UCL > Provost and Vice Provost Offices
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/1476369
Downloads since deposit
75Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item