Scalable Software Verification
Module 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, you 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.
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
(IL06) explain the reasoning techniques underpinning the SL tools
(ILO7) 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-6: three weeks
- semi-automatic tools for specialist developers: Smallfoot, Gillian
- automatic tool for the general developer: Facebook Infer
- underlying techniques: symbolic execution, frame inference, bi-abduction
Concurrent Separation Logics, IL07: one week
- original concurrent SL: coarse-grained concurrent programs
- modern concurrent SLs: fine-grained concurrent programs
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 industry.
An online service will be used as a discussion forum for the module.
Assessments
Two coursework exercises (20%); one two-hour exam (80%).
There will be detailed feedback on the coursework exercises, including comprehensive written answers, written feedback on your individual submission, and an in-class question and answer session with an explanation of the common pitfalls and suggestions for improvement.