An Asynchronous soundness theorem for concurrent separation logic

Paul-André Melliès, Léo Stefanesco

Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. In this paper, we develop a concurrent and interactive a…