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, 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 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.

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

Pre-requisites

Recommended: COMP40003 Logic , COMP40006 Reasoning about Programs, (JMC: COMP40012 Logic and Reasoning), COMP50003 Models of Computation.

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.

The Piazza Q&A web service will be used as an open online 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.

Reading list

Basic Separation Logic

  • Local Reasoning about Programs that Alter Data Structures

    P. O'Hearn, J. Reynolds, H. Yang

    CSL 2001: Computer Science Logic

  • Separation logic: a logic for shared mutable data structures

    Reynolds, J.C.

    Logic in Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on IEEE

Techniques for Separation-Logic-Based Tools

  • Symbolic Execution with Separation Logic

    Josh Berdine,Cristiano Calcagno,Peter W. O’Hearn

    APLAS 2005: Programming Languages and Systems Springer, Berlin, Heidelberg

  • A Local Shape Analysis Based on Separation Logic

    Dino Distefano,Peter W. O’Hearn,Hongseok Yang

    TACAS 2006 Springer, Berlin, Heidelberg

  • Compositional Shape Analysis by Means of Bi-Abduction

    Calcagno, Cristiano ; Distefano, Dino ; O'Hearn, Peter W ; Yang, Hongseok

    Journal of the ACM (JACM) ACM

Separation Logic for Concurrency

  • Resources, concurrency, and local reasoning

    O’hearn, Peter W.

    Theoretical Computer Science Elsevier B.V.

  • Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)

    Da Rocha Pinto, Pedro ; Dinsdale-Young, Thomas ; Gardner, Philippa

    Electronic Notes in Theoretical Computer Science Elsevier B.V.

Program Logics (general literature)

Module leaders

Dr Petar Maksimovic
Professor Philippa Gardner