On the Complexity of Pointer Arithmetic in Separation Logic (an extended version)

James Brotherston, Max Kanovich

We investigate the complexity consequences of adding pointer arithmetic to separation logic. Specifically, we study extensions of the points-to fragment of symbolic-heap separation…