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 COMP *tbc* "the New Logic Module name still undecided", (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
Recommended: COMP40003 Logic , COMP40006 Reasoning about Programs, (JMC: COMP40012 Logic and Reasoning), COMP50003 Models of Computation.
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.
The Piazza Q&A web service will be used as an open online 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.
Basic Separation Logic
Local Reasoning about Programs that Alter Data Structures
CSL 2001: Computer Science Logic
Separation logic: a logic for shared mutable data structures
Logic in Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on IEEE
Techniques for Separation-Logic-Based Tools
Symbolic Execution with Separation Logic
APLAS 2005: Programming Languages and Systems Springer, Berlin, Heidelberg
A Local Shape Analysis Based on Separation Logic
TACAS 2006 Springer, Berlin, Heidelberg
Compositional Shape Analysis by Means of Bi-Abduction
Journal of the ACM (JACM) ACM
Separation Logic for Concurrency
Resources, concurrency, and local reasoning
Theoretical Computer Science Elsevier B.V.
Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)
Electronic Notes in Theoretical Computer Science Elsevier B.V.
Program Logics (general literature)
Second edition., Cambridge University Press
Cambridge University Press
Cambridge University Press
Program Logics for Certified Compilers / [electronic resource] Andrew W. Appel ; with contributions by Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, Xavier Leroy.
Cambridge University Press,
Module leadersDr Petar Maksimovic
Professor Philippa Gardner