Hoare Logic and Model Checking
Small note on errata in past exam questions and the exercise sheet for Hoare Logic.
Update: fixed typo on slide 11 of lecture 7 (definition of initial temporal model).
Supervision materials and past exam information are taken from the 20/21 course.
Revision class
| Lecture | 1-up | 4-up | Remarks | |||
| Revision class |
Part 1: Hoare logic
Slides
| Lecture | 1-up | 4-up | Remarks | |||
| 1: Introduction to Hoare logic | Slide 31: fixed formula layout compared to printout. | |||||
| 2: Examples in Hoare logic | Why3 web UI and Why3 manual | |||||
| 3: Formalising the semantics of Hoare logic | ||||||
| 4: Introduction to separation logic | John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. | |||||
| 5: Verifying abstract data types in separation logic | ||||||
| 6: Extending Hoare logic |
Supervision questions (Hoare logic)
Jean Pichon Pharabod's 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; students should be comfortable with finding and proving loop invariants for abstract data types in separation logic. Please see the above note on errata. 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
Slides
| Lecture | 1-up | 4-up | Remarks | |||
| 7: Introduction to model checking | Fixed typo on slide 11 | |||||
| 8: Temporal logic | ||||||
| 9: Temporal logic (continued) | ||||||
| 10: Implementing model checking | OCaml code for naive model checker wwctlmc.ml | |||||
| 11: Relating temporal models | The last slide includes some links for model checkers. |
Supervision questions (Model checking)
Jean Pichon Pharabod's exercise sheet is largely based on previous sheets due to Mike Gordon (link -- exercises and solution notes) and Dominic Mulligan (link) (notation differs).
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 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) 2019 Paper 9 Question 8
- (Hoare Logic and Model Checking) 2018 Paper 7' Question 7
(note that the department pages list "Paper 7'" separately from "Paper 7") - (Hoare Logic and Model Checking) 2017 Paper 9 Question 13 (notation differs)
- (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 (the question should say "for every reachable state s", as pointed out by an anonymous student)
- (Temporal Logic and Model Checking) 2011 Paper 7 Question 10 not part (c)
- (Temporal Logic and Model Checking) 2011 Paper 9 Question 11 only part (b)
Older questions (beware that sometimes notation differs from that 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)(i)
- (Specification and Verification II) 2006 Paper 7 Question 7 only (c)
- (Specification and Verification II) 2005 Paper 7 Question 7 only part (a)
- (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 (symbolic model checking not covered in detail this year)
- (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