UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Biabduction (and related problems) in array separation logic

Brotherston, J; Kanovich, M; Gorogiannis, N; (2017) Biabduction (and related problems) in array separation logic. In: De Moura, L, (ed.) Automated Deduction – CADE 26: 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6–11, 2017, Proceedings. (pp. pp. 472-490). Springer: Cham, Switzerland. Green open access

[img]
Preview
Text
array_biabduction_final.pdf - ["content_typename_Accepted version" not defined]
Available under License : See the attached licence file.

Download (480kB) | Preview

Abstract

We investigate array separation logic (ASLASL), a variant of symbolic-heap separation logic in which the data structures are either pointers or arrays, i.e., contiguous blocks of memory. This logic provides a language for compositional memory safety proofs of array programs. We focus on the biabduction problem for this logic, which has been established as the key to automatic specification inference at the industrial scale. We present an NPNP decision procedure for biabduction in ASLASL, and we also show that the problem of finding a consistent solution is NPNP-hard. Along the way, we study satisfiability and entailment in ASLASL, giving decision procedures and complexity bounds for both problems. We show satisfiability to be NPNP-complete, and entailment to be decidable with high complexity. The surprising fact that biabduction is simpler than entailment is due to the fact that, as we show, the element of choice over biabduction solutions enables us to dramatically reduce the search space.

Type: Proceedings paper
Title: Biabduction (and related problems) in array separation logic
Event: 26th International Conference on Automated Deduction (CADE 26)
Dates: 08 August 2017 - 11 August 2017
ISBN-13: 9783319630465
Open access status: An open access version is available from UCL Discovery
DOI: 10.1007/978-3-319-63046-5_29
Publisher version: https://doi.org/10.1007/978-3-319-63046-5_29
Language: English
Additional information: This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions.
Keywords: Separation logic, Arrays, Biabduction, Entailment, Complexity
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: http://discovery.ucl.ac.uk/id/eprint/1559241
Downloads since deposit
31Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item