Course pages 2012–13
Hoare Logic
Material is examinable if it is presented in lectures!
Exercises and past exam questions
- The first 16 exercises in this exercise list have some solution notes.
- There are also some past exam questions that are relevant to this course.
Reading
- Some background reading (latest version incorporates suggestions and corrections from John Wickerson)
- Further reading (optional)
Slides
The whole set of slides is available both as a single document:
- [A3 postscript (for projection) | A4 pdf | A4 pdf (4 slides per page) | printed handout (won't be updated)]
or split into sections:
- Introduction to formal methods and Hoare logic.
[ A3 for projection | A4 for printing (PDF) ] - Formal Specification.
[ A3 for projection | A4 for printing (PDF) ] - Introduction to Primitive Axioms and Rules for Partial Correctness.
[ A3 for projection | A4 for printing (PDF) ] - Further Primitive Rules. Invariants.
[ A3 for projection | A4 for printing (PDF) ] - Soundness and Completeness.
[ A3 for projection | A4 for printing (PDF) ] - Derived Rules; Mechanizing Hoare Logic.
[ A3 for projection | A4 for printing (PDF) ] - Proving Programs Terminate.
[ A3 for projection | A4 for printing (PDF) ] - More constructs: arrays, blocks and FOR-commands.
[ A3 for projection | A4 for printing (PDF) ] - Refinement.
[ A3 for projection | A4 for printing (PDF) ] - Pointers, the Frame Problem and Separation Logic.
[ A3 for projection | A4 for printing (PDF) ]
Material from lectures
Occasionally, I sketch a proof during lectures. Here are some of those proof sketches.
Interesting links
- Floyd's orbituary; his seminal 1967 paper Assigning meanings to programs
- Hoare's home page at Microsoft; 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
- Why - a generic verification condition generator
- VCC - a Verifier for Concurrent C (web interface)
- Scalable Specification and Reasoning: Technical Challenges for Program Logic by Peter O'Hearn
- Verified Software: A Grand Challenge
- Microsoft SLAM, TERMINATOR and SLAyer projects.
- Wikipedia article on Material Implication, the Paradoxes of Material Implication and some classic fallacies
- Bibliographic Notes on Hoare Logic compiled by John Reynolds, and the slides for his course at CMU
- Collection of Software Bugs and Software Glitches
- Peter Homeier's Sunrise system
- Design by Contract (a paper by Gary T. Leavens and Yoonsik Cheon)
- Separation logic inspired startup Monoidics and their tool INFER.
- Starting from about 28:26 minutes into this video there is a nice introduction to metamathematics (soundness, completeness, Goedel's theorem, Turing machines etc.).
Related courses
- Programming Logics and Software Verification (MPhil ACS)
- Specification and Verification I (predecessor Part II course)