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: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). (pp. 25 - 42).

Full text not available from this repository.

Abstract

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
DOI:10.1007/978-3-642-23702-7_7
UCL classification:UCL > School of BEAMS > Faculty of Engineering Science > Computer Science

Archive Staff Only: edit this record