Department of Computer Science and Technology

Course pages 2017–18

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

The (updated: 25 May 2018) slides are available as a single pdf (4-up), or as individual sets of slides for each lecture:

Lecture Slides Interesting reading and links
Lecture 1: Introduction to Hoare logic pdf (1-up)
pdf (4-up) 		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 (1-up)
pdf (4-up) 		Glynn Winskel. The Formal Semantics of Programming Languages.
Chapters 6-7.
Lecture 3: Examples, loop invariants and total correctness pdf (1-up)
pdf (4-up)
Lecture 4: Mechanised program verification pdf (1-up)
pdf (4-up) 		The Why3 verification system.
Lecture 5: Separation logic pdf (1-up)
pdf (4-up) 		John Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures
Lecture 6: Examples in separation logic pdf (1-up)
pdf (4-up) 		Peter O'Hearn. Resources, Concurrency and Local Reasoning

Errata

The above PDFs give the updated and corrected version of all the lecture slides from Part 1. For reference, here are the slides as printed. Thanks to Mistral Contrastin, Victor Gomes, Joe Isaacs, Ian Orton, and Domagoj Stolfa for reporting mistakes.

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.

Past exam questions (Hoare logic)

Care should be taken when revising using past exam papers; a change of emphasis in the course content (starting 2016/17) caused new material to be added, while material that was focused on in earlier years is now only been skimmed over. 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 sub-components of exam questions from previous years are still relevant:

  • (Hoare Logic and Model Checking) Paper 7, Question 8, 2017.
  • (Hoare Logic and Model Checking) Parts (a), (b), (c), (d), (e), and (f); Paper 7, Question 8, 2016.
  • (Hoare Logic) Part (b) and subsection (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

Handout

  • Lecture slides (as PDF, 1-up)
  • Lecture slides (as PDF, 4-up)
  • An additional slide (as PDF) on counter-example generation for model checking with explicit-state representation (logically fits just before slide 52).
  • A useful discussion on CTL vs LTL xpressibility>
  • Errata/Lacunae:
    • Slide 31: the title is negated: we are trying to show that "States *not* satisfying NotAt11 are unreachable from (0,0,0,0)" i.e. we cannot reach (1,1,x,y) from (0,0,0,0).
    • Slide 63: I could have explained the mnemonic for F,G,X:
      "G: (G)lobally holds; F: At some point in the (F)uture; X: In the ne(X)t state"
      and mentioned the alternative Box and Diamond notation used in the 2016/17 notes.
    • Slide 69-71. The word "starting" is ambiguous. Here it means "if we start at", or "rebasing π to start at i steps along"
    • Slide 117 on bisimulation, point 3: (i) the final R' in point 3 should be an R; (ii) the (s1' \in S) should be (s1' \in S').
      Also it would be clearer if the "exists" state their domains, i.e. (point 2) \exists s1' \in S' and (point 3) \exists s1 \in S.

Supervision questions (model checking)

  • Some exercises due to Mike Gordon and solution notes.
    Note that the current lecture course does not cover Q14 and Q15.

Past exam questions (model checking)

Care should be taken when revising using past exam papers; a change of emphasis in the course content (starting 2016/17) caused new material to be added, while material that was focused on in earlier years is now only been skimmed over. 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 sub-components of exam questions from previous years are still relevant:

Older questions (beware that sometimes notation differs from that used in the current course)