27 citations · 29 across the 3 of their papers we have counts for
4 papers · 1 filter
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…
Size Relationships in Abstract Cyclic Entailment Systems
Reuben N. S. Rowe, James Brotherston
A cyclic proof system generalises the standard notion of a proof as a finite tree of locally sound inferences by allowing proof objects to be potentially infinite. Regular infinite…
Biabduction (and Related Problems) in Array Separation Logic
James Brotherston, Nikos Gorogiannis, Max Kanovich
We investigate array separation logic (ASL), a variant of symbolic-heap separation logic in which the data structures are either pointers or arrays, i.e., contiguous blocks of allo…
Classical BI: Its Semantics and Proof Theory
James Brotherston, Cristiano Calcagno
We present Classical BI (CBI), a new addition to the family of bunched logics which originates in O'Hearn and Pym's logic of bunched implications BI. CBI differs from existing bunc…