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.
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