[Colloquium] Talk by John Reynolds, CMU, 10/8/03

[Margery Ishmael]

------------------------------------------------------------------------ 
-----

DEPARTMENT OF COMPUTER SCIENCE - TALK

Wednesday, October 8, 2003 at 2:30 pm in Ryerson 251

------------------------------------------------------------------------ 
------

Speaker:  John Reynolds, Carnegie Mellon University
http://www-2.cs.cmu.edu/afs/cs.cmu.edu/user/jcr/www/

Title: Separation Logic: A Logic for Shared Mutable Data Structures

ABSTRACT:
In joint work with Peter O'Hearn and others, based on early
ideas of Burstall, we have developed an extension of Hoare logic
that permits reasoning about low-level imperative programs that
use shared mutable data structure.

The simple imperative programming language is extended with commands
(not expressions) for accessing and modifying shared structures, and
for explicit allocation and deallocation of storage.  Assertions are
extended by introducing a ``separating conjunction'' that asserts that
its subformulas hold for disjoint parts of the heap, and a closely
related ``separating implication''.  Coupled with the inductive
definition of predicates on abstract data structures, this extension
permits the concise and flexible description of structures with
controlled sharing.

We will survey the current development of this program logic, including
extensions that permit unrestricted address arithmetic; we will also
discuss promising future directions.

Host: David MacQueen

*Refreshments will follow the talk in Ryerson 255*

People in need of assistance should call 773-834-8977 in advance.



=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Margery Ishmael
Secretary to the Chairman
Department of Computer Science
The University of Chicago
1100 E. 58th Street, Chicago, IL. 60637-1581
tel. 773.834.8977 fax. 773.702.8487
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=