Department of Computer Science and Technology

Hoare Logic and Model Checking

# Hoare Logic and Model Checking

As discussed in the revision lecture, I upload a small note on errata in past exam questions and the exercise sheet. I will try to update this in case there are more.

Supervision materials and past exam information are taken from the 20/21 course.

## Revision class

 Lecture 1-up 4-up Remarks Revision class pdf pdf

## Part 1: Hoare logic

### Slides

 Lecture 1-up 4-up Remarks 1: Introduction to Hoare logic pdf pdf 2: Examples in Hoare logic pdf pdf Why3 web UI and Why3 manual 3: Formalising the semantics of Hoare logic pdf pdf 4: Introduction to separation logic pdf pdf John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. 5: Verifying abstract data types in separation logic pdf pdf Note update on slide 19 compared to handout. 6: Extending Hoare logic pdf pdf Note small updates compared to handout.

### 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, 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

### Slides

 Lecture 1-up 4-up Remarks 7: Introduction to model checking pdf pdf 8: Temporal logic pdf pdf Fixed typo on slide 21. 9: Temporal logic (continued) pdf pdf Note minor udpates with respect to the handouts. 10: Implementing model checking pdf pdf Note fixes compared to handouts. OCaml code for naive model checker wwctlmc.ml 11: Relating temporal models pdf pdf Note changes compared to handouts. 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 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 in the current course):