# Department of Computer Science and Technology

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.

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

• © 2019 Department of Computer Science and Technology, University of Cambridge
Information provided by Dr Jean Pichon