Separation logic assertions describe "states" consisting of a "store" and a "heap", roughly corresponding to the state of local (or "stack-allocated") variables and "dynamically-allocated" objects in common programming languages such as C and Java. A store formula_1 is a function mapping variables to values. A heap formula_2 is a partial function mapping memory addresses to values. Two heaps formula_2 and formula_4 are "disjoint" (denoted formula_5) if their domains do not overlap (i.e., for every memory address formula_6, at least one of formula_7 and formula_8 is undefined).