Programming Logics and Software Verification

Convenor: Mike Gordon
Module code: L19
Lecturers: (alphabetical order) Josh Berdine, Byron Cook, Mike Dodds, Mike Gordon, Matthew Parkinson, John Wickerson.
Taken by: MPhil ACS
Number of lectures: 16
Lecture location: Room SW01, WGB
Lecture times: 17:00 on Tue & Thu starting Thu Jan 20, 2011

Summary: Provides a detailed overview of the current state of the art in verification of programming languages such as Java and C.
(Official syllabus)

The first five lectures were by given by Mike Gordon and contained introductory material on Hoare logic taken from the Part II course Hoare Logic.

The rest of the course was presented by Mike Dodds and John Wickerson from the Computer Laboratory and by Byron Cook and Josh Berdine from Microsoft Research Cambridge.

20 Jan: Mike Gordon    - Partial Correctness, Hoare Logic
25 Jan: Mike Gordon    - Mechanisation using verification conditions
27 Jan: Mike Gordon    - Weakest preconditions, Strongest postconditions, Total Correctness
01 Feb: Mike Gordon    - Semantics, Soundness, Completeness
03 Feb: Mike Gordon    - Introduction to Separation Logic
08 Feb: John Wickerson - More Separation Logic
10 Feb: Matt Parkinson - Procedures, Modules and the Hypothetical Frame Rule
15 Feb: Matt Parkinson - Abstract Predicates and Objects
17 Feb: Josh Berdine   - Symbolic Execution and Smallfoot (paper1, paper2)
22 Feb: Josh Berdine   - Tools, Abstract Interpretation, etc. (paper3, paper4, paper5)
24 Feb: Mike Dodds     - Concurrent Separation Logic
01 Mar: Byron Cook     - Termination
03 Mar: Mike Dodds     - More Concurrent Separation Logic (includes earlier slides)
08 Mar: John Wickerson - Rely-Guarantee
10 Mar: John Wickerson - RGSep
15 Mar: Mike Dodds     - Deny Guarantee

Additional material, papers etc

Josh Berdine writes:

   The paper to consult for rearrangement and symbolic execution is
   "Symbolic Execution with Separation Logic"

   For abstraction the relevant one is "A local shape analysis based on
   separation logic"

   For the material on procedures, a paper to
   look at is "Interprocedural Shape Analysis with Separated Heap
   Abstractions" (  
   The tabulation algorithm that is not specific to separation logic is
   described in "Precise interprocedural dataflow analysis via graph
   reachability" (  
   For the hierarchical data structures material, see "Shape Analysis for
   Composite Data Structures"
Mike Dodds recommends the following papers:
   Resources, Concurrency and Local Reasoning

   Permission Accounting in Separation Logic
and the two papers he cited in the Deny Guarantee lectures are:
   Deny-Guarantee Reasoning

   Concurrent Abstract Predicates


The course will be assessed by an open book written test at 14:00-16:00 on 27 April. The paper will have six questions of which you are required to answer four.

We have prepared a mock exam paper to aid your revision (error in Question 1 corrected on 05-04-2011).

The answers to the questions below are intended to give an idea of the minimum sort of thing that we would give good marks to.

In the test on April 27, questions may be set on anything covered in the course except for material presented in Byron Cook's March 1 lecture on Termination and in Mike Dodds' March 15 lecture on Deny Guarantee. The rubric on the test paper includes the following:

  The setters of the questions in this paper hope that there are no
  errors or obscurities. However, if you think there are, then you
  should explain the problem in your answer and state carefully what
  interpretation or correction you are assuming. Credit will be given
  for successfully coping with such problems.

The following preliminary list of papers are recommended reading for preparing for the test. It is possible that a few more papers will be added to this list.

   Mike Gordon. Lecture notes for the CST Part II course "Hoare Logic".
   Available from:
   John Reynolds. Separation Logic: A Logic for Shared Mutable Data
   Structures. LICS 2002. Available from:

   Peter O’Hearn, John Reynolds and Hongseok Yang. Local Reasoning about
   Programs that Alter Data Structures. CSL 2001. Available from:

   Viktor Vafeiadis. Modular fine-grained concurrency
   verification. Chapters 1-3 only. PhD thesis, University of Cambridge,
   2007. Available from:

   Viktor Vafeiadis. Concurrent separation logic and operational
   semantics. MFPS, 2011. Available from:

   O'Hearn et al, Resources, Concurrency and Local Reasoning:
   Bornat et al, Permission Accounting in Separation Logic:

   P.W. O'Hearn, H. Yang, J.C. Reynolds. Separation and Information Hiding. 
   In POPL 04. Available from: