Biabduction (and related problems) in array separation logic
Conference paper
Brotherston, J., Gorogiannis, N. and Kanovich, M. 2017. Biabduction (and related problems) in array separation logic. International Conference on Automated Deduction. Gothenburg 08 - 11 Aug 2017 Springer. https://doi.org/10.1007/978-3-319-63046-5_29
Type | Conference paper |
---|---|
Title | Biabduction (and related problems) in array separation logic |
Authors | Brotherston, J., Gorogiannis, N. and Kanovich, M. |
Abstract | We investigate array separation logic (\mathsf {ASL}), 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 \mathsf {NP} decision procedure for biabduction in \mathsf {ASL}, and we also show that the problem of finding a consistent solution is \mathsf {NP}-hard. Along the way, we study satisfiability and entailment in \mathsf {ASL}, giving decision procedures and complexity bounds for both problems. We show satisfiability to be \mathsf {NP}-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. |
Research Group | Foundations of Computing group |
Conference | International Conference on Automated Deduction |
ISSN | 0302-9743 |
ISBN | |
Hardcover | 978-3-319-63046-5 |
Publisher | Springer |
Publication dates | |
11 Jul 2017 | |
Publication process dates | |
Deposited | 02 Oct 2017 |
Accepted | 23 Apr 2017 |
Output status | Published |
Accepted author manuscript | |
Copyright Statement | The final publication is available at Springer via https://doi.org/10.1007/978-3-319-63046-5_29 |
Additional information | Cite this paper as: |
Digital Object Identifier (DOI) | https://doi.org/10.1007/978-3-319-63046-5_29 |
Language | English |
Book title | Automated Deduction – CADE 26 |
https://repository.mdx.ac.uk/item/87316
Download files
18
total views4
total downloads0
views this month1
downloads this month