Subject: [Fwd: rinard@cag.lcs.mit.edu] Talk
From: Mitchell Wand (wand@ccs.neu.edu)
Date: Fri Sep 28 2001 - 08:42:04 EDT
------- start of forwarded message (RFC 934 encapsulation) -------
X-SpamBouncer: 1.4 (8/24/01)
X-SBPass: NoBounce
X-SBClass: OK
From: rinard@cag.lcs.mit.edu
To: alex.garthwaite@sun.com, david.detlefs@east.sun.com, kfoury@cs.bu.edu,
matthias@ccs.neu.edu, wand@ccs.neu.edu
Subject: Talk
Date: Thu, 27 Sep 2001 15:32:13 -0400 (EDT)
Hi guys. Here is a talk next week that may be of interest to you.
Please feel free to pass the announcement along if you think it is
appropriate.
Best Regards,
Martin
Colloquium on Computer Architecture and Compiler Technology Series
Monday, October 1, 2001
NE43-518
3-5 PM
Refreshments served
- ------------------------------------------
VAULT: Enforcing High-Level Protocols in Low-Level Software
By Manuel Fahndrich
This talk introduces VAULT, a new programming language being designed
at Microsoft Research. There are two reasons for creating a new
language. First, to combine programmer control over data layout and
lifetime as in C or C++ with the memory safety of ML or Java. Second,
to capture usage rules in interface descriptions in order to check
both clients and the implementation itself. Usage rules enable
stating for example the valid order of function calls and the
ownership transfers of data. Both memory safety and usage rules are
expressed as part of VAULT's type system. Our initial experience
shows that the VAULT type system can enforce many important rules
between device drivers and the W2K kernel. Some examples of rules are:
mutual exclusion of memory accesses between kernel threads,
allocation/deallocation rules of dynamically allocated data, and
interrupt level restrictions.
Manuel Fahndrich is a researcher at Microsoft Research in Redmond,
Washington, since November 1998. He received his B.E. in computer
engineering from
the Ecole Polytechnique Federal de Lausanne in Switzerland in 1993,
his M.Sc., and PhD. in computer science from the University of
California at Berkeley in 1995 and 1999 respectively.
His research interests are in applying formal systems to proving
program properties. He has built BANE, the Berkeley Analysis Engine
which is used to express and implement a number of program analysis
problems, ranging from pointer analysis to escaping exception
analysis. Current interests are focused on partial specifications, in
particular of heap properties, and the integration of specifications
and programming languages.
------- end -------
This archive was generated by hypermail 2b28 : Fri Sep 28 2001 - 08:43:06 EDT