Course pages 2016–17
Hoare Logic and Model Checking
The course text is "Logic in Computer Science" (second edition) by Huth and Ryan. Copies are available from the library, with at least one deposited in the reserved books section.
Part 1: Hoare logic
Lecture  Slides  Suggested reading and interesting links 
Lecture 1: Introduction to Hoare logic  pdf (1up) pdf (4up) 
R. W. Floyd. Assigning meanings to programs. 1967. C. A. R. Hoare. An axiomatic basis for computer programming. 1969. 
Lecture 2: Semantics of Hoare logic  pdf (1up) pdf (4up) 
Glynn Winskel. The Formal Semantics of Programming Languages. Chapters 67. 
Lecture 3: Examples, loop invariants and total correctness  pdf (1up) pdf (4up) 

Lecture 4: Mechanised program verification  pdf (1up) pdf (4up) 
The Why3 verification system. 
Lecture 5: Separation logic  pdf (1up) pdf (4up) 
John Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures 
Lecture 6: Examples in separation logic  pdf (1up) pdf (4up) 
Peter O'Hearn. Resources, Concurrency and Local Reasoning 
Errata
Below is a list of known mistakes from the lecture slides and exercise questions. An updated and corrected version of all the lecture slides from Part 1 is available here.
 Lecture 1, "Auxiliary variables" slide: there is a typo in the postcondition of the Hoare triple; the second conjunct of the post condition should read "Y ≤ X ⇒ Z = X" instead of "Y ≤ X ⇒ X = Y".
 Lecture 2, "The assertion language" slide: the universal quantifier should bind a logical variable rather than a program variable and thus by convention should be written "∀x.P" with a lowercase "x" instead of "∀X.P".
 Lecture 2, proof of substitution property for variable case: It should say "Case E1 ≡ V'" instead of "Case E1 ≡ V".
 Lecture 3, total correctness backwardsreasoning rules for while loops: the rules should use metavariable B for a boolean expression instead of the metavariable S.
 Lecture 5, "Pointer assignment" slide: The command should be [E_1] := E_2 in all the reduction rules. (Thanks to Mistral Contrastin for pointing out this typo.)
 Lecture 5, "Examples of separation logic assertions", example 3: The assertion "X > E1 * Y > E2" only holds if X and Y alias and E1 = E2.
 Lecture 6, "Representation predicates", definition of the list predicate: there is a typo in the inductive case of the list predicate; the "v" in the definition of list(head, x::β) should be "x".
 Lecture 6, "Swap example", detailed proof of the first triple: there was a missing step in the proof; after applying the heapdereference rule we first existentially quantify the auxiliary variable "a" before applying the ruleofconsequence.
 Lecture 56: the operational semantics I sketched for WHILE extended with pointers allows expressions to fault in case of invalid pointer arithmetic. However, the separation logic I presented assumes that expressions always evaluate to a nonfault value and is unsound unless all expressions always evaluate to nonfault values. (Thanks to Ian Orton for spotting this mistake.)
 Additional exercises, exercise 3: there was a typo in the postcondition of the Hoare triple. The postcondition is supposed to be P[E/V] instead of P[E/X] (Thanks to Victor Gomes for spotting this mistake).
Supervision questions
Below is a list of suggested supervision questions for the Hoare logic part of the course. Supervisors are encouraged to pick a varied subset of questions, with at least a couple of questions that require finding a loop invariant.
 Exercises 2, 3, 4, 5, 7, 8, 9, 10, 11, 12, 17, 18, 19, 20, 31 from Mike Gordon's exercise set
 Additional exercises
Past exam questions
Care should be taken when revising using past exam papers, as due to the change of emphasis in the course content this year material that was focussed on in previous years has only been skimmed over this year, whilst new material has been added. Further, the current Hoare Logic and Model Checking course is a descendent of many similar courses offered by the Computer Laboratory in previous years, which often had radically different syllabuses. However, the following exam subcomponents of exam questions from previous years are still relevant:
 (Hoare Logic and Model Checking) Parts (a), (b), (c), (d), (e), and (f); Paper 7, Question 8, 2016.
 (Hoare Logic) Part (b) and subquestion (i) of Part (c); Paper 7, Question 7, 2015.
 (Hoare Logic) Part (a); Paper 7, Question 7, 2014.
 (Hoare Logic) Parts (a), (b), (c), and (d); Paper 7, Question 7, 2013.
 (Hoare Logic) Parts (a), (b), (c), (d), (e); Paper 8, Question 8, 2013.
 (Hoare Logic) Parts (a) and (b); Paper 8, Question 8, 2012.
 (Hoare Logic) Parts (b) and (c); Paper 8, Question 2, 2011.
 (Hoare Logic) Parts (a) and (b); Paper 7, Question 6, 2011.
 (Specification and Verification I) Part (a); Paper 7, Question 14, 2010.
 (Specification and Verification I) Parts (a), (b), (d) and (e); Paper 7, Question 14, 2009.
 (Specification and Verification I) Parts (a) and (b); Paper 8, Question 16, 2008.
 (Specification and Verification I) Parts (a), (c), (e) and (i); Paper 7, Question 6, 2007.
 (Specification and Verification I) Parts (a), (b), (c), (d), (f), (g) and (h); Paper 7, Question 6, 2006.
Part 2: model checking
Though not a course text, for more indepth reading on subject matter covered in our lectures (and much more), Principles of Model Checking by Baier and Katoen is recommended. Copies of this book are also available from the university libraries.
Lecture  Slides  Suggested reading 
Lecture 7: Introduction and formal methods  pdf (1 up) pdf (4 up) 
Section 3.1 of "Logic in Computer Science" Knight Capital trading bug 
Lecture 8: Linear Temporal Logic (LTL)  pdf (1 up) pdf (4 up) 
Section 3.2 of "Logic in Computer Science" Subsection 3.6.3 of "Logic in Computer Science" 
Lecture 9: A brief look at NuSMV  pdf (1 up) pdf (4 up) 
Section 3.3 of "Logic in Computer Science" NuSMV 2.6 tutorial NuSMV 2.6 user manual 
Lecture 10: Computation Tree Logic (CTL)  pdf (1 up) pdf (4 up) 
Section 3.4 of "Logic in Computer Science" 
Lecture 11: Model checking for Computation Tree Logic  pdf (1 up) pdf (4 up) 
Subsection 3.6.1 of "Logic in Computer Science" (Note that "Logic in Computer Science" handles all modalities directly, instead of using ENF.) 
Lecture 12: Loose ends  pdf (1 up) pdf (4 up) 
Section 3.5 of "Logic in Computer Science" Counterexample Guided Abstraction Refinement, by Clarke, Grumberg, et al. (Brief) overview of symmetry reduction, by Miller and Donaldson 
Supervision questions
One and a half supervisions are dedicated to the model checking component of the course. An exercise sheet with suggested supervision questions for use in this component can be found here. The questions cover the whole range of topics covered by the course, and supervisors are encouraged to pick a varied subset of questions, with at least one question being a practical exercise in the use of NuSMV. Note that as the content of the course has changed slightly this year, the supervision questions provided above are likely to be more reflective of potential exam questions than past exam questions, which are tailored to older material.
Errata, and clarifications
In the lecture slides (with thanks to various nameless students, Mistral Contrastin, Ian Orton, Dylan McDermott, and Stella Lau):
 Lecture 8, slide 13: "U" should read "UNTIL"
 Lecture 8, slide 26: "prefix" should read "suffix"
 Lecture 9, slide 31: "G(x_input & R.output > y_output)" should read "G(!x_input & R.output > !y_output)"
 Lecture 10, slide 12: note that in first example of "impossible formulae", small phi ranges over path formulae. Note also that state formulae are more "fundamental" than path formulae (as CTL formulae pick out states in a model), and the entry point for the mutually recursive grammar of the two is taken to be the grammar for state formulae.
 Lecture 10, slide 38: the first "bottom" on the first line of the slide should be a "top"
 Lecture 10, slide 39: on the right hand side of the equivalence for the universaluntil modality, the first Phi should be a Psi.
 Lecture 12, slide 19: quantifiers on "all reachable states" were messed up, leading to an incorrect definition.
 Lecture 12, slide 22: second bullet point was rewritten to make clear correct order of quantifiers.
 Lecture 12, slide 32: "important LTL equivalences and normal forms" are not examinable material, and have not been lectured this year. This line should be ignored.
In the supervision questions (with thanks to Jean Pichon for spotting some of these):
 Question 2.4: "flicking temperate and pressure" should read "flicking temperature and pressure".
 Question 2.6: this question should state "show that the simulation preorder is indeed a preorder on models". As it is written, the question is unanswerable (as the property you are trying to show does not hold).
 Question 6.3: "Impressed with your earlier success, modelling a simple crossroads" should read "Impressed with your earlier success modelling a simple crossroads".
 Question 6.4: To answer this question you need to use NuSMV's CTL model checking facilities. Use the check_ctlspec command in interactive mode, or the CTLSPEC block embedded in an SMV file, to check CTL properties with NuSMV. Note that in SMV syntax, A is used to encode forall, and E is used to encode exists, in CTL formulae.
Past exam questions
Care should be taken when revising using past exam papers, as due to the change of emphasis in the course content this year material that was focussed on in previous years has only been skimmed over this year, whilst new material has been added. Further, the current Hoare Logic and Model Checking course is a descendent of many similar courses offered by the Computer Laboratory in previous years, which often had radically different syllabuses. As a result, the types of questions asked in the supervision sheet provided above are a better guide for directed supervision than previous exam questions. However, the following exam subcomponents of exam questions from previous years are still relevant:
 (Hoare Logic and Model Checking) Paper 9, Question 12, 2016.
 (Temporal Logic and Model Checking) Paper 8, Question 6, 2015.
 (Temporal Logic and Model Checking) Paper 8, Question 8, 2014.
 (Temporal Logic and Model Checking) Paper 7, Question 13, 2012.
 (Temporal Logic and Model Checking) Paper 9, Question 12, 2012.
 (Temporal Logic and Model Checking) Paper 7, Question 10, 2011.
Previous exam questions (back to 2008) that where only subcomponents of the exam question are still relevant, are:
 (Specification and Verification II) Paper 7, Question 15, 2010. Only parts (c) and (d) are relevant to the current course.
 (Specification and Verification II) Paper 7, Question 15, 2009. Only part (a) is relevant to the current course.
 (Specification and Verification II) Paper 9, Question 13, 2009. Only parts (e), (g), (h), and (i) are relevant to the current course.
 (Specification and Verification II), Paper 9 Question 8, 2008. Only part (c) is relevant to the current course.
 (Specification and Verification II), Paper 7, Question 7, 2006. Only parts (a) and (c) are relevant to the current course. Note for part (e) of this question: you will be expected to know some advantages/disadvantages of model checking but not necessarily how model checking compares against theorem proving specifically.
All past papers can be accessed here.
Model checking software
Binaries and a source distribution for the NuSMV model checker can be found here. I use version 2.6.0 in lectures, though any recent version of the model checker will suffice.
Though not covered in lectures, I encourage you to play around with as many model checking tools as you can. In particular, you may be interested in the C Bounded Model Checker (CBMC), a verification tool for C and C++ programs that is based on model checking technology. CBMC is able to automatically establish array bounds are respected, and pointers are correctly handed, in a given C or C++ program by unrolling the program's control flow graph and applying bounded model checking to search for property violations. CBMC can be downloaded here.