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…