Imperial College London


Faculty of EngineeringDepartment of Computing

Professor of Theoretical Computer Science



+44 (0)20 7594 8292p.gardner Website




453Huxley BuildingSouth Kensington Campus




Scalable Software Verification - COMP70023


Software verification has come of age: proof assistants are mature; verification techniques and tools are tractable; and real-world programs are verified both in academia and industry. A key breakthrough came with separation logic, which introduced compositional reasoning about heap-manipulating programs. The aim of this course is to enable  students to reason about 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 about the 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.

Recommended pre-requisites: for the M.Eng students,  an interest in COMP40018 Discrete Mathematics, Logic and Reasoning,  (JMC: COMP40012 Logic and Reasoning), COMP50003 Models of Computation (the part on semantics); for the MSc students, either some experience in  formal reasoning about programs  or rigorous programming skills or a good knowledge of algorithms and  a strength in mathematics.


Course Leader