Course pages 2016–17

Hoare Logic and 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.

Part 1: Hoare logic

Errata

Below is a list of known mistakes from the lecture slides and exercise questions. An updated and corrected version of all the lecture slides from Part 1 is available here.

• Lecture 1, "Auxiliary variables" slide: there is a typo in the postcondition of the Hoare triple; the second conjunct of the post condition should read "Y ≤ X ⇒ Z = X" instead of "Y ≤ X ⇒ X = Y".
• Lecture 2, "The assertion language" slide: the universal quantifier should bind a logical variable rather than a program variable and thus by convention should be written "∀x.P" with a lowercase "x" instead of "∀X.P".
• Lecture 2, proof of substitution property for variable case: It should say "Case E1 ≡ V'" instead of "Case E1 ≡ V".
• Lecture 3, total correctness backwards-reasoning rules for while loops: the rules should use meta-variable B for a boolean expression instead of the meta-variable S.
• Lecture 5, "Pointer assignment" slide: The command should be [E_1] := E_2 in all the reduction rules. (Thanks to Mistral Contrastin for pointing out this typo.)
• Lecture 5, "Examples of separation logic assertions", example 3: The assertion "X |-> E1 * Y |-> E2" only holds if X and Y alias and E1 = E2.
• Lecture 6, "Representation predicates", definition of the list predicate: there is a typo in the inductive case of the list predicate; the "v" in the definition of list(head, x::β) should be "x".
• Lecture 6, "Swap example", detailed proof of the first triple: there was a missing step in the proof; after applying the heap-dereference rule we first existentially quantify the auxiliary variable "a" before applying the rule-of-consequence.
• Lecture 5-6: the operational semantics I sketched for WHILE extended with pointers allows expressions to fault in case of invalid pointer arithmetic. However, the separation logic I presented assumes that expressions always evaluate to a non-fault value and is unsound unless all expressions always evaluate to non-fault values. (Thanks to Ian Orton for spotting this mistake.)
• Additional exercises, exercise 3: there was a typo in the postcondition of the Hoare triple. The postcondition is supposed to be P[E/V] instead of P[E/X] (Thanks to Victor Gomes for spotting this mistake).

Supervision questions

Below is 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 at least a couple of questions that require finding a loop invariant.

• Exercises 2, 3, 4, 5, 7, 8, 9, 10, 11, 12, 17, 18, 19, 20, 31 from Mike Gordon's exercise set
• Additional exercises

Past exam questions

Care should be taken when revising using past exam papers, as due to the change of emphasis in the course content this year material that was focussed on in previous years has only been skimmed over this year, whilst new material has been added. 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 subcomponents of exam questions from previous years are still relevant:

• (Hoare Logic and Model Checking) Parts (a), (b), (c), (d), (e), and (f); Paper 7, Question 8, 2016.
• (Hoare Logic) Part (b) and subquestion (i) of Part (c); Paper 7, Question 7, 2015.
• (Hoare Logic) Part (a); Paper 7, Question 7, 2014.
• (Hoare Logic) Parts (a), (b), (c), and (d); 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

Though not a course text, for more in-depth reading on subject matter covered in our lectures (and much more), Principles of Model Checking by Baier and Katoen is recommended. Copies of this book are also available from the university libraries.

Supervision questions

One and a half supervisions are dedicated to the model checking component of the course. An exercise sheet with suggested supervision questions for use in this component can be found here. The questions cover the whole range of topics covered by the course, and supervisors are encouraged to pick a varied subset of questions, with at least one question being a practical exercise in the use of NuSMV. Note that as the content of the course has changed slightly this year, the supervision questions provided above are likely to be more reflective of potential exam questions than past exam questions, which are tailored to older material.

Errata, and clarifications

In the lecture slides (with thanks to various nameless students, Mistral Contrastin, Ian Orton, Dylan McDermott, and Stella Lau):

• Lecture 8, slide 13: "U" should read "UNTIL"
• Lecture 8, slide 26: "prefix" should read "suffix"
• Lecture 9, slide 31: "G(x_input & R.output -> y_output)" should read "G(!x_input & R.output -> !y_output)"
• Lecture 10, slide 12: note that in first example of "impossible formulae", small phi ranges over path formulae. Note also that state formulae are more "fundamental" than path formulae (as CTL formulae pick out states in a model), and the entry point for the mutually recursive grammar of the two is taken to be the grammar for state formulae.
• Lecture 10, slide 38: the first "bottom" on the first line of the slide should be a "top"
• Lecture 10, slide 39: on the right hand side of the equivalence for the universal-until modality, the first Phi should be a Psi.
• Lecture 12, slide 19: quantifiers on "all reachable states" were messed up, leading to an incorrect definition.
• Lecture 12, slide 22: second bullet point was rewritten to make clear correct order of quantifiers.
• Lecture 12, slide 32: "important LTL equivalences and normal forms" are not examinable material, and have not been lectured this year. This line should be ignored.

In the supervision questions (with thanks to Jean Pichon for spotting some of these):

• Question 2.4: "flicking temperate and pressure" should read "flicking temperature and pressure".
• Question 2.6: this question should state "show that the simulation preorder is indeed a preorder on models". As it is written, the question is unanswerable (as the property you are trying to show does not hold).
• Question 6.3: "Impressed with your earlier success, modelling a simple crossroads" should read "Impressed with your earlier success modelling a simple crossroads".
• Question 6.4: To answer this question you need to use NuSMV's CTL model checking facilities. Use the check_ctlspec command in interactive mode, or the CTLSPEC block embedded in an SMV file, to check CTL properties with NuSMV. Note that in SMV syntax, A is used to encode forall, and E is used to encode exists, in CTL formulae.

Past exam questions

Care should be taken when revising using past exam papers, as due to the change of emphasis in the course content this year material that was focussed on in previous years has only been skimmed over this year, whilst new material has been added. 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. As a result, the types of questions asked in the supervision sheet provided above are a better guide for directed supervision than previous exam questions. However, the following exam subcomponents of exam questions from previous years are still relevant:

• (Hoare Logic and Model Checking) Paper 9, Question 12, 2016.
• (Temporal Logic and Model Checking) Paper 8, Question 6, 2015.
• (Temporal Logic and Model Checking) Paper 8, Question 8, 2014.
• (Temporal Logic and Model Checking) Paper 7, Question 13, 2012.
• (Temporal Logic and Model Checking) Paper 9, Question 12, 2012.
• (Temporal Logic and Model Checking) Paper 7, Question 10, 2011.

Previous exam questions (back to 2008) that where only subcomponents of the exam question are still relevant, are:

• (Specification and Verification II) Paper 7, Question 15, 2010. Only parts (c) and (d) are relevant to the current course.
• (Specification and Verification II) Paper 7, Question 15, 2009. Only part (a) is relevant to the current course.
• (Specification and Verification II) Paper 9, Question 13, 2009. Only parts (e), (g), (h), and (i) are relevant to the current course.
• (Specification and Verification II), Paper 9 Question 8, 2008. Only part (c) is relevant to the current course.
• (Specification and Verification II), Paper 7, Question 7, 2006. Only parts (a) and (c) are relevant to the current course. Note for part (e) of this question: you will be expected to know some advantages/disadvantages of model checking but not necessarily how model checking compares against theorem proving specifically.

All past papers can be accessed here.

Model checking software

Binaries and a source distribution for the NuSMV model checker can be found here. I use version 2.6.0 in lectures, though any recent version of the model checker will suffice.

Though not covered in lectures, I encourage you to play around with as many model checking tools as you can. In particular, you may be interested in the C Bounded Model Checker (CBMC), a verification tool for C and C++ programs that is based on model checking technology. CBMC is able to automatically establish array bounds are respected, and pointers are correctly handed, in a given C or C++ program by unrolling the program's control flow graph and applying bounded model checking to search for property violations. CBMC can be downloaded here.