Revisiting concurrent separation logic

Pedro Soares, António Ravara, Simão Melo de Sousa

We present a new soundness proof of Concurrent Separation Logic (CSL) based on a structural operational semantics (SOS). We build on two previous proofs and develop new auxiliary n…