Programming logics for dynamic data structures

Lecturer

Uday Reddy, University of Birmingham

Abstract

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

http://www-2.cs.cmu.edu/afs/cs.cmu.edu/project/fox-19/member/jcr/wwwaac2003/aac.html
Thorsten Altenkirch
Last modified: Thu Feb 5 09:37:29 GMT 2004