A banner for the unit in the colours of Norton Commander

COMSM0067

Lectures

Week Day Topic Resources
1 Monday Welcome + Judgements Slides, Notes, Proofs Note, Lecture1
  Tuesday Induction Notes, Lecture2, Week1BP, Takeaways
2 Monday Statics Notes, Lecture3
  Tuesday Inversion & Structural Rules Notes, Lecture4, Week2BP, Takeaways
3 Monday Dynamics Notes, Lecture5
  Tuesday Type safety Notes, Lecture6, Week3BP, Takeaways
4 Monday Functions, Effects and Calling Mechanisms Notes, Lecture7, Week4BP, Takeaways
  Tuesday Hoare Logic I: Triples and rules Lecture8
5 Monday Hoare Logic II: Invariants and weakest preconditions Lecture9, Takeaways
  Tuesday Separation Logic I: The heap, the separating conjunction, and the frame rule Lecture10
6 Consolidation Week    
7 Monday Separation Logic II: Inductive predicates, and a proof that pays for itself Takeaways
  Tuesday Symbolic Execution: Under-approximation, and the logic of bugs Takeaways
8 Monday From Separation Logic to Rust: Ownership as a type system — and what it costs Takeaways
  Tuesday Ownership in Context*  

*This end of the course will allow you to consolidate what you have learnt during the course in the exciting setting of a real research paper! This will be presented by Tom Divers, PhD student of the Bristol Programming Languages Research Group