Context-Aware Separation Logic

Roland Meyer, Thomas Wies, Sebastian Wolff

Separation logic is often praised for its ability to closely mimic the locality of state updates when reasoning about them at the level of assertions. The prover only needs to conc…