BRICS · Contents · Programme · References

Separation Logic

A BRICS Mini-Course
November 11, 13, 18, 20, 25 and 27, December 2 and 4, 2003

Lectures by
John C. Reynolds, John.Reynolds@cs.cmu.edu
School of Computer Science, Carnegie Mellon University, Pittsburgh, USA


Course Contents

Separation logic is an extension of Hoare logic for reasoning about programs that use shared mutable data structures. We will survey the current development of this logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, recursive procedures, and shared-variable concurrency. We will also discuss promising future directions.

Some acquaintance with predicate logic will be assumed.

Programme

Tuesday November 11, 2003, 15:15-17:00 in Auditorium D4

Thursday November 13, 2003, 15:15-17:00 in Auditorium D4

Tuesday November 18, 2003, 15:15-17:00 in Auditorium D4

Thursday November 20, 2003, 15:15-17:00 in Auditorium D4

Tuesday November 25, 2003, 15:15-17:00 in Auditorium D4

Thursday November 27, 2003, 15:15-17:00 in Auditorium D4

Tuesday December 2, 2003, 15:15-17:00 in Auditorium D4

Thursday December 4, 2003, 15:15-17:00 in Auditorium D4

References

Papers and notes to be distributed in class.