Biabduction (and related problems) in array separation logic

DOI10.1007/978-3-319-63046-5_29zbMath1496.03125arXiv1607.01993OpenAlexW2964228214MaRDI QIDQ2405270

James Brotherston, Nikos Gorogiannis, Max I. Kanovich

Publication date: 22 September 2017

Full work available at URL: https://arxiv.org/abs/1607.01993

zbMATH Keywords

complexityarraysentailmentseparation logicbiabduction

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Data structures (68P05)

Related Items (6)

Decision Procedure for Entailment of Symbolic Heaps with Arrays ⋮ Unnamed Item ⋮ Compositional satisfiability solving in separation logic ⋮ Unnamed Item ⋮ An adaptation-complete proof system for local reasoning about cloud storage systems ⋮ Reasoning about block-based cloud storage systems via separation logic

This page was built for publication: Biabduction (and related problems) in array separation logic