Tractable Reasoning In A Fragment Of Separation Logic
CONCUR'11: Proceedings of the 22nd international conference on Concurrency theory(2011)
摘要
In 2004, Berdine, Calcagno and O'Hearn introduced a fragment of separation logic that allows for reasoning about programs with pointers and linked lists. They showed that entailment in this fragment is in coNP, but the precise complexity of this problem has been open since. In this paper, we show that the problem can actually be solved in polynomial time. To this end, we represent separation logic formulae as graphs and show that every satisfiable formula is equivalent to one whose graph is in a particular normal form. Entailment between two such formulae then reduces to a graph homomorphism problem. We also discuss natural syntactic extensions that render entailment intractable.
更多查看译文
关键词
Normal Form, Polynomial Time, Black Node, Separation Logic, Graph Homomorphism
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络