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]
- Some exercises due to Mike Gordon and solution notes to the first 16.
- Suggested questions for supervision:
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
- Mike Gordon's book-style course notes on Hoare Logic
- Optional further reading (short bibliography) on (a) Hoare Logic and (b) Model Checking
- The discontinued MPhil course Programming Logics and Software Verification
- Recent paper on Hoare logic for weak memory
- Alan Turing describes his work on soundness, completeness, Gödel's theorem, Turing machines etc.
- Floyd's orbituary; his seminal 1967 paper Assigning meanings to programs
- Wikipedia article on Hoare; his seminal 1969 paper An axiomatic basis for computer programming
- Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems by Edmund M. Clarke Jr.
- Zune bug explained in detail
- Why3 - a generic verification condition generator
- Scalable Specification and Reasoning: Technical Challenges for Program Logic by Peter O'Hearn
- Verified Software: A Grand Challenge
- Wikipedia article on Material Implication, the Paradoxes of Material Implication and some classic fallacies
- Collection of Software Bugs and Software Glitches
- The VCC verifier can be downloaded from vcc.codeplex.com or tried at rise4fun.com/vcc
- Peter Homeier's Sunrise system
- Design by Contract (a paper by Gary T. Leavens and Yoonsik Cheon)
- CakeML: a verification friendly dialect of SML
- Software Model Checking Takes Off
- Formal verification of chess endgame databases
- Modal logics and mu-calculi: an introduction
- Microsoft SLAM, T2 temporal prover (code) and SLAyer projects.