Computer Laboratory

Course pages 2015–16

Hoare Logic and Model Checking

Course information: (updated 18 May 2016)

  • Course slides (as PDF, 1-up)
  • Course slides (as PDF, 4-up)
  • Revision slides for Logic and Proof (PDF, 1-up)
  • Revision slides for Logic and Proof (PDF, 4-up)
  • Larry Paulson's definition of truth in first-order logic from the Logic and Proof course
  • Errata/Lacunae:
    • Slide 26: the labels "(SEQ)" and "(IF)" are interchanged.
    • Slide 82 (line 3): formally there should be a ";" after C_1.
    • Slide 83 (line 2): the program should be "R:=X; X:=Y; Y:=R" (not "R:=X; X:=Y; X:=R").
    • There are some residual uses of the word "statement" to mean "formula" (I've tried to use the word "formula" consistently for wffs in logic).
    • Slides 44-49, 51 and 59 use the letter "S" for boolean expression when the rest of the slides use the letter "B".
    • slide 86, typo (missing "]") on line 5: ⊢ {P} C {Q[E/V*]*}
    • Slide 101: Cut-and-paste typo: "but this doesn’t in general define wlp(C,Q) as a finite formula" should refer to "sp(C,P)" instead of "wlp(C,Q)".
    • Slide 144: "An unfortunate read of X in C2 might see an odd integer but this is not possible in C1." C1 and C2 should be swapped in this sentence.
    • Slide 161: the adjective 'total' for a relation R is somewhat non-standard.
      Here it is used to mean 'left-total, i.e. "forall s. exists t. R s t" (as in 'total function'); a 'total relation' usually means "forall s,t. R s t or R t s" (as in 'total order') -- see the Wikipedia page on Binary relations.
    • Slide 169: the title is negated: we are trying to show that "States *not* satisfying NotAt11 are unreachable from (0,0,0,0)" i.e. we cannot reach (1,1,x,y) from (0,0,0,0).
    • Slide 255 (not lectured) on bisimulation, point 3: (i) the final R' in point 3 should be an R; (ii) the (s1' \in S) should be (s1' \in S').
      Also it would be clearer if the "exists" state their domains, i.e. (point 2) \exists s1' \in S' and (point 3) \exists s1 \in S.
    • It might be useful to say Design by Contract (e.g. Eiffel) is an example of Correct-by-Construction software development
    • The Logic and Proof revision notes should be incorporated in the main course notes; there is also a typo on slide 4: "interesting in time" should be "interested in time".
    • The Wikipedia page on Model checking isn't very helpful for an introduction. Anyone want to improve it?

Annotated Past Tripos questions

  • Here is a list of past exam questions that are relevant to this course (annotated as to which parts are appropriate for the current course). [NOW UPDATED FOR 2015/16]

Exercises: [first half of the course]

Exercises: [second half of the course]

  • Some exercises due to Mike Gordon and solution notes.
    Note that the current lecture course does not cover Q14 and Q15.

Course book

  • Logic in Computer Science: Modelling and Reasoning about Systems. Michael Huth and Mark Ryan. Cambridge University Press, Second Edition 2004. ISBN: 0 521 54310. Web page: http://www.cs.bham.ac.uk/research/lics/

Further Reading and Interesting links