Department of Computer Science and Technology

Course pages 2019–20

Hoare Logic and Model Checking

Part 1: Hoare logic

The (updated) 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) 		The Why3 verification system.
isqrt.why3.
Lecture 2: Examples in Hoare logic pdf (1-up)
pdf (4-up)
Lecture 3: Formalising the semantics of Hoare logic pdf (1-up)
pdf (4-up) 		Glynn Winskel. The Formal Semantics of Programming Languages.
Chapters 6-7.
Lecture 4: Introduction to separation logic pdf (1-up)
pdf (4-up) 		John Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures
Lecture 5: Verifying abstract data types in separation logic pdf (1-up)
pdf (4-up)
Lecture 6: Extending Hoare logic pdf (1-up)
pdf (4-up) 		The VeriFast verification system, list.c
Facebook's Infer bug-finding system, arr.c
Peter O'Hearn. Resources, Concurrency and Local Reasoning

Supervision questions

The Hoare Logic exercise sheet has 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 the aim that students are comfortable with finding and proving loop invariants for abstract data types in separation logic.

Mike Gordon's exercise set contains some additional exercises.

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 being 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 8, Question 7, 2019.
  • (Hoare Logic and Model Checking) Paper 9, Question 7, 2018.
  • (Hoare Logic and Model Checking) Paper 7, Question 8, 2017.
  • (Hoare Logic and Model Checking) Paper 7, Question 8, 2016.
  • (Hoare Logic) Part (b) and subsection (i) of Part (c); Paper 7, Question 7, 2015.
  • (Hoare Logic) 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

Lecture Slides Interesting reading and links
Lecture 7: Introduction to Model Checking pdf (1-up)
pdf (4-up)
Lecture 8: Temporal logics pdf (1-up)
pdf (4-up)
Lecture 9: Using model checking Demo goat.tla
peterson.pml
good.smv
Lecture 10: Relating temporal models pdf (1-up)
pdf (4-up) 		Recording updated 2020/05/28 (see below).
tictactoeabs.pml
abstraction.c
Lecture 11: Implementing model checking pdf (1-up)
pdf (4-up) 		wwctlmc.ml
Lecture 12: Revisiting model checking Demo. goat.als
ringElection2.als

The recording of Lecture 10 was updated on 2020/05/28 to fix the dicussion of the need to restrict what states properties are allowed in the preservation by simulation theorem.

The supporting material document contains the definitions, in order, for reference.

Supervision questions (model checking)

  • Some exercises due to Mike Gordon and solution notes.
  • Some exercises due to Dominic Mulligan (notation differs).
  • The TLA+ examples page contains a few puzzles (with solutions): Missionaries and Cannibals, Car Talk, N queens, Prisoners, Die Hard 3 puzzle, etc.

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)