Subject: RE: [Fwd: rinard@cag.lcs.mit.edu] Talk
From: Paul Steckler (steck@ccs.neu.edu)
Date: Fri Sep 28 2001 - 10:44:50 EDT
I believe the same talk is to be given at NEPLS.
-- Paul
> -----Original Message-----
> From: Mitchell Wand [mailto:wand@ccs.neu.edu]
> Sent: Friday, September 28, 2001 8:42 AM
> To: pl-seminar@ccs.neu.edu
> Subject: [Fwd: rinard@cag.lcs.mit.edu] Talk
>
> ------- 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 - 10:45:19 EDT