Scalable Software Verification - COMP70023
Aims
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.
Role
Course Leader