## Separation Logic: Scalable Reasoning about Programs - COMP97005

### Aims

To enable the students to reason compositionally about sequential and concurrent heap-manipulating programs using separation logic, both by exploring the underlying theory and by working with cutting-edge academic and industrial analysis tools. The fact that the reasoning is compositional means that it scales.

The theoretical part of the course will revolve around a simple While language, whereas the practical part will touch on real-world languages such as Java, JavaScript and C.

More specifically, the students will:

- gain an in-depth understanding of the theory underpinning separation logic, why it works and why it is correct;
- use separation logic to specify and verify sequential programs, focusing on standard data structures and their operations;
- learn how to work with academic and industrial tools based on separation logic;
- gain basic familiarity with concurrent separation logics, in particular their theory and their application to concurrent data-structure algorithms.

### Role

Course Leader

## Separation Logic: Scalable Reasoning about Programs - COMP97006

### Aims

To enable the students to reason compositionally about sequential and concurrent heap-manipulating programs using separation logic, both by exploring the underlying theory and by working with cutting-edge academic and industrial analysis tools. The fact that the reasoning is compositional means that it scales.

The theoretical part of the course will revolve around a simple While language, whereas the practical part will touch on real-world languages such as Java, JavaScript and C.

More specifically, the students will:

- gain an in-depth understanding of the theory underpinning separation logic, why it works and why it is correct;
- use separation logic to specify and verify sequential programs, focusing on standard data structures and their operations;
- learn how to work with academic and industrial tools based on separation logic;
- gain basic familiarity with concurrent separation logics, in particular their theory and their application to concurrent data-structure algorithms.

### Role

Course Leader