Hoare Logic and Model Checking

Small note on errata in past exam questions and the exercise sheet for Hoare Logic.

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

Part 1: Hoare logic

Slides

Lecture		1-up		4-up		Remarks
1: Introduction to Hoare logic		pdf		pdf		Slide 31: fixed formula layout compared to printout.
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
6: Extending Hoare logic		pdf		pdf

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.