Models of Computation - CO240
The course intends to make sure that all students establish a stronger foundation in the more theoretical side of Computer Science, thus better preparing them for the courses that will follow in the fourth year.
The course will focus on teaching students the fundamental skills involved in dealing with abstract systems and constructing proofs, through both teaching and exercises.
Separation Logic: Local Reasoning about Programs - CO404
The aim of this course is to introduce the student to separation logic and associated verifications tools.
Summary of Course
In the late 1960s, Tony Hoare developed Hoare logic, a formal system with a set of rules for reasoning rigorously about the correctness of imperative programs that alter the variable state. However, Hoare logic is not good at reasoning about imperative programs that alter the heap state, since the reasoning does not scale. In 2001, building on Hoare's work and early ideas from Burstall, O'Hearn and Reynolds introduced separation logic, in which the reasoning does scale.