The complexity of abduction for separated heap abstractions.
Presented at: UNSPECIFIED.
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:||Conference item (UNSPECIFIED)|
|Title:||The complexity of abduction for separated heap abstractions|
|UCL classification:||UCL > School of BEAMS > Faculty of Engineering Science
UCL > School of BEAMS > Faculty of Engineering Science > Computer Science
Archive Staff Only