Abduction, the problem of discovering hypotheses that sup-port a conclusion, has mainly been studied in the context of philosoph-ical logic and Artificial Intelligence. Recently, it was used in a compo-sitional program analysis based on separation logic that discovers (par-tial) 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.
展开▼
