Course pages 2018–19
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) |
|
| Lecture 2: Examples in Hoare logic |
pdf (1-up) pdf (4-up) |
The Why3 verification system. |
| 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) |
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.
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 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
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.
Handout
- Lecture slides (as PDF, 1-up) (as PDF, 4-up)
- Slides 46-52 were not lectured and can be skipped.
- Lecture 1 supplement (as PDF, 1-up) (as PDF, 4-up)
- A condensed recap of important concepts from lecture 1 (slides 1-32).
- Lecture 3 supplement (as PDF, 1-up) (as PDF, 4-up)
- Board examples worked through during lecture 3 (slides 60-77).
- Lecture 4 supplement (as PDF, 1-up) (as PDF, 4-up)
- Board examples worked through during lecture 4 (slides 78-94).
- A useful discussion on CTL vs LTL expressibility
Supervision questions (model checking)
- Some exercises due to Mike Gordon and solution notes.
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:
- (Hoare Logic and Model Checking) 2016 Paper 9 Question 12
- (Temporal Logic and Model Checking) 2015 Paper 8 Question 6 not part (e)
- (Temporal Logic and Model Checking) 2014 Paper 8 Question 8
- (Temporal Logic and Model Checking) 2012 Paper 7 Question 13
- (Temporal Logic and Model Checking) 2012 Paper 9 Question 12
- (Temporal Logic and Model Checking) 2011 Paper 7 Question 10 not part (c)
- (Temporal Logic and Model Checking) 2011 Paper 9 Question 11 only parts (b) and (c)
Older questions (beware that sometimes notation differs from that used in the current course)
- (Specification and Verification II) 2009 Paper 7 Question 15 not covered, but part (a) is worth discussing
- (Specification and Verification II) 2007 Paper 9 Question 8 only parts (a) and (c)
- (Specification and Verification II) 2006 Paper 7 Question 7 not part (d) and part (b) only sketchily covered
- (Specification and Verification II) 2005 Paper 7 Question 7 only parts (a) and (b) (the rest of the question is `enrichment')?
- (Specification and Verification II) 2003 Paper 7 Question 7 not parts (d) and (e)
- (Specification and Verification II) 2002 Paper 7 Question 2
- (Specification and Verification II) 2000 Paper 8 Question 13
- (Specification and Verification II) 1999 Paper 8 Question 13 not really part of the course as taught, but useful background on BDDs
- (Specification and Verification II) 1998 Paper 7 Question 11 not the second point