Imperial College London

ProfessorPhilippaGardner

Faculty of EngineeringDepartment of Computing

Professor of Theoretical Computer Science
 
 
 
//

Contact

 

+44 (0)20 7594 8292p.gardner Website

 
 
//

Location

 

453Huxley BuildingSouth Kensington Campus

//

Summary

 

Models of Computation - CO240

Aims

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.

Role

Course Leader

Separation Logic: Local Reasoning about Programs - CO404

Aims

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.
 
This course will provide a whirl-wind tour of separation logic, its verification tools and cutting-edge research on reasoning about concurrent programs.  Separation logic was introduced to reason about shared mutable data structures represented in the heap: in particular, to catch memory overruns and null-pointer dereferencing. It has been used to reason about C, Java and JavaScript programs, and algorithms for shared-memory concurrency.  There are many academic verification tools, such as Smallfoot, Verifast and Abductor, and the industrial tool Infer (see http://fbinfer.com/), developed by a team led by Peter O'Hearn at Facebook.  As well as Facebook, Infer is used by Instagram, kiuwan, oculus, Spotify, UBER, WhatsApp, Marks and Spencer, and Sky.

Role

Course Leader