Tractable reasoning in a fragment of separation logic
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 sh...
| Main Authors: | , , , , |
|---|---|
| Format: | Conference item |
| Published: |
2011
|