[PRL] Fwd: [temp] Seminars Digest, Vol 86, Issue 3

[Mitchell Wand]

Possibly of interest....

---------- Forwarded message ----------
From: <seminars-request at lists.csail.mit.edu>
Date: Fri, Feb 5, 2010 at 9:00 AM
Subject: [temp] Seminars Digest, Vol 86, Issue 3
To: seminars at lists.csail.mit.edu


From: Csail Event Calendar <eventcalendar at csail.mit.edu>
To: seminars at csail.mit.edu
Date: Fri, 05 Feb 2010 00:01:02 -0500
Subject: TALK:Friday 2-12-10 PRAGMATIC TYPESTATE VERIFICATION WITH
PERMISSIONS

PRAGMATIC TYPESTATE VERIFICATION  WITH PERMISSIONS
Speaker: Jonathan Aldrich
Speaker Affiliation: Carnegie Mellon University
Host: Martin Rinard
Host Affiliation: MIT-CSAIL

Date: 2-12-2010
Time: 2:00 PM - 3:00 PM
Refreshments: 1:45 PM
Location: 32-D463, Star Conference Room

ABSTRACT
Object-oriented libraries often define usage protocols that clients must
follow in order for the system to work properly.  These protocols may be
poorly documented and difficult to follow, causing errors and significant
lost
productivity in software development.

We are exploring a new approach to verifying object protocols using
permissions.  These permissions track not only the current "typestate" of an
object in its protocol, but an abstraction of what operations other aliases
might perform on the object and what invariants must remain true. Developers
annotate their code with state and permission information, which can be
automatically and soundly checked for consistency.  Our approach is fully
modular, yet allows substantial reasoning about objects even when they are
aliased by multiple clients.  I will discuss extensions to check protocols
in
concurrent systems, our practical experience with the system, and current
work
toward a new programming language based on typestate.

BIO
Jonathan Aldrich is Associate Professor of Computer Science at Carnegie
Mellon University.  He is the director of CMU's undergraduate minor program
in
Software Engineering, and teaches courses in programming languages, software
engineering and program analysis. Dr. Aldrich joined the CMU faculty after
completing a Ph.D. at the University of Washington and a B.S. at Caltech.

Aldrich's research contributions include verifying architectural structure
and secure information flow, modular formal reasoning about code, and API
protocol safety.  For his work on architecture and information flow, Aldrich
received a 2006 NSF CAREER award and the 2007 Dahl-Nygaard Junior Prize,
given
annually for a significant technical contribution to object-oriented
programming.

Relevant URL(S):
For more information please contact: Mary McDavitt, 617-253-9620,
mmcdavit at csail.mit.edu
-------------- next part --------------
HTML attachment scrubbed and removed