Separation Logic: Scalable Reasoning about Programs

Module 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.

Learning outcomes

After completing the course, the students will be able to:

(ILO1) evaluate the design choices underpinning SL for While
(ILO2) establish the correctness of SL for While with respect to the While operational semantics
(ILO3) adapt SL for While to other simple programming languages and justify the adaptation
(ILO4) design abstractions, create specifications, and produce rigorous correctness proofs for standard sequential data structures and their associated algorithms
(ILO5) use several state-of-the-art academic and industrial tools based on SL, whose analysis ranges from semi-automatic verification to automatic lightweight bug-finding
(ILO6) apply concurrent SLs to specify and verify simple concurrent data-structure algorithms

Module syllabus

Core Separation Logic (SL), ILO1-4: three weeks

  • SL assertion language and entailment
  • SL for a simple While language
  • specification and verification of data-structure algorithms
  • soundness of SL with respect to the While operational semantics

Tools and Techniques, ILO5: two weeks

  • semi-automatic tools for specialist developers: Smallfoot, Gillian
  • automatic tool for the general developer: Facebook Infer
  • techniques: symbolic execution, frame inference, bi-abduction

Concurrent Separation Logics, IL06: two weeks

  • original concurrent SL: coarse-grained concurrent programs
  • modern concurrent SLs: fine-grained

Teaching methods

Seven weeks of four hours of intertwined lectures and tutorials, plus an additional two-hour revision lecture. The material is taught through traditional lectures, backed up by tutorial exercises and lab tool sessions, designed to reinforce understanding of the comprehensive course notes. The tutorial exercises will be accompanied by model answers, and the tutorials and labs will be supported by Graduate Teaching Assistants. The tutorials and labs will not be assessed. The tutorial questions will include variations on past exam questions, in preparation for the final exam. One of the labs will be organised by Facebook London.

Assessments

The module will feature two courseworks, published in weeks four and six. The courseworks will be a natural progression of the weekly tutorial exercises given in the class. They will be done individually. The students will have ten days to complete the coursework, which will then be marked and returned the following week.

(ILO5) will be assessed informally, in tutorials.

The students will submit their coursework by hand. Submissions will be marked by GTAs and given back the following week. There will be detailed feedback on the coursework exercises, including comprehensive model answers, written feedback on individual submissions, and an in-class question-and-answer session with an explanation of the common pitfalls and suggestions for improvement.

Reading list

Module leaders

Professor Philippa Gardner