UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

The complexity of abduction for separated heap abstractions

Gorogiannis, N; Kanovich, M; O'Hearn, PW; (2011) The complexity of abduction for separated heap abstractions. In: (pp. pp. 25-42).

Full text not available from this repository.


Abduction, the problem of discovering hypotheses that support a conclusion, has mainly been studied in the context of philosophical logic and Artificial Intelligence. Recently, it was used in a compositional program analysis based on separation logic that discovers (partial) pre/post specifications for un-annotated code which approximates memory requirements. Although promising practical results have been obtained, completeness issues and the computational hardness of the problem have not been studied. We consider a fragment of separation logic that is representative of applications in program analysis, and we study the complexity of searching for feasible solutions to abduction. We show that standard entailment is decidable in polynomial time, while abduction ranges from NP-complete to polynomial time for different sub-problems. © 2011 Springer-Verlag Berlin Heidelberg.

Type: Proceedings paper
Title: The complexity of abduction for separated heap abstractions
ISBN-13: 9783642237010
DOI: 10.1007/978-3-642-23702-7_7
UCL classification: UCL > School of BEAMS
UCL > School of BEAMS > Faculty of Engineering Science
URI: http://discovery.ucl.ac.uk/id/eprint/1363229
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item