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 GuaranteeAdditional material, papers etc
Josh Berdine writes:
The paper to consult for rearrangement and symbolic execution is "Symbolic Execution with Separation Logic" (http://research.microsoft.com/pubs/64175/execution.pdf). For abstraction the relevant one is "A local shape analysis based on separation logic" (http://www.dcs.qmul.ac.uk/~hyang/paper/spaceinvader-long.pdf). For the material on procedures, a paper to look at is "Interprocedural Shape Analysis with Separated Heap Abstractions" (http://research.microsoft.com/pubs/67601/interproc.pdf). The tabulation algorithm that is not specific to separation logic is described in "Precise interprocedural dataflow analysis via graph reachability" (http://www.cs.wisc.edu/wpis/papers/popl95.pdf). For the hierarchical data structures material, see "Shape Analysis for Composite Data Structures" (http://research.microsoft.com/pubs/73868/safcds.pdf).Mike Dodds recommends the following papers:
Resources, Concurrency and Local Reasoning Permission Accounting in Separation Logicand the two papers he cited in the Deny Guarantee lectures are:
Deny-Guarantee Reasoning Concurrent Abstract Predicates
Assessment
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: http://www.cl.cam.ac.uk/~mjcg/Teaching/2011/CST/Hoare/HoareLogic/Notes.pdf John Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. LICS 2002. Available from: http://www.cs.cmu.edu/~jcr/seplogic.pdf Peter O’Hearn, John Reynolds and Hongseok Yang. Local Reasoning about Programs that Alter Data Structures. CSL 2001. Available from: http://www.dcs.qmul.ac.uk/~ohearn/papers/localreasoning.pdf Viktor Vafeiadis. Modular fine-grained concurrency verification. Chapters 1-3 only. PhD thesis, University of Cambridge, 2007. Available from: http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-726.html Viktor Vafeiadis. Concurrent separation logic and operational semantics. MFPS, 2011. Available from: http://www.mpi-sws.org/~viktor/cslsound/ O'Hearn et al, Resources, Concurrency and Local Reasoning: http://www.dcs.qmul.ac.uk/~ohearn/papers/concurrency.pdf Bornat et al, Permission Accounting in Separation Logic: http://www.eis.mdx.ac.uk/staffpages/r_bornat/papers/permissions_paper.pdf P.W. O'Hearn, H. Yang, J.C. Reynolds. Separation and Information Hiding. In POPL 04. Available from: http://www.dcs.qmul.ac.uk/~ohearn/papers/separation-and-hiding.pdf