Programming logics for dynamic data structures


Uday Reddy, University of Birmingham


Dynamic data structures are those allocated dynamically and addressed via pointers are references. They include data structures like linked lists, trees and graphs, and all objects in object-oriented languages like Java. Traditional Hoare Logic-based reasoning does not work well for such structures because it does not capture modularity. Great strides on this problem have been made in recent years through the development of Separation Logic by Reynolds, O'Hearn and others, and it is an active research area. This course covers all aspects of Separation Logic at its present stage, including reasoning about data structures, ownership representation, concurrency and automatic verification.

Reference material
Thorsten Altenkirch
Last modified: Thu Feb 5 09:37:29 GMT 2004