Scalable Software Verification
- 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.
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
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
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.
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.
Module leadersDr Petar Maksimovic
Professor Philippa Gardner