A sound and complete proof system for separation logic (part 1)

Source abstract

<i> </i> Download the PDF version of this article 1 Introduction In this article we have another look at the proof system for separation logic that is introduced in the first author's PhD thesis [5] (publicly defended on Thursday, May 23rd, 2024). By separation logic we mean the logic behind the assertion language used in Reynolds' logic, the program logic for reasoning about the correctness of pointer programs that was introduced in