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
TypeConference paper
TitleBiabduction (and related problems) in array separation logic
AuthorsBrotherston, 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 GroupFoundations of Computing group
ConferenceInternational Conference on Automated Deduction
ISSN0302-9743
ISBN
Hardcover978-3-319-63046-5
PublisherSpringer
Publication dates
Print11 Jul 2017
Publication process dates
Deposited02 Oct 2017
Accepted23 Apr 2017
Output statusPublished
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:
Brotherston J., Gorogiannis N., Kanovich M. (2017) Biabduction (and Related Problems) in Array Separation Logic. In: de Moura L. (eds) Automated Deduction – CADE 26. CADE 2017. Lecture Notes in Computer Science, vol 10395. Springer, Cham

Digital Object Identifier (DOI)https://doi.org/10.1007/978-3-319-63046-5_29
LanguageEnglish
Book titleAutomated Deduction – CADE 26
Permalink -

https://repository.mdx.ac.uk/item/87316

Download files


Accepted author manuscript
  • 24
    total views
  • 5
    total downloads
  • 3
    views this month
  • 1
    downloads this month

Export as