13th Estonian Winter School in Computer Science (EWSCS)
XIII Eesti Arvutiteaduse Talvekool

Palmse, Estonia, March 2-7, 2008

Nick Benton

Microsoft Research
Cambridge, UK

Modelling and Reasoning about State

Abstract

Reasoning about programs that use dynamically allocated mutable storage is surprisingly difficult, especially in the presence of higher-order features such as first-class functions or code pointers. The hard problems in coming up with accurate models or usable program logics for languages that include these awkward features have many names, including aliasing, encapsulation, interference, privacy, ownership and freshness. I'll talk about some recent work that tries to use a relatively small number of ideas (chiefly relational parametricity and separation) to address these issues in several different contexts, including giving the semantics of ML-like languages, proving the correctness of static analyses and optimizing transformations, and specifying and verifying machine code programs.

Course materials

Valid CSS! Valid XHTML 1.0 Strict Last changed March 12, 2008 23:52 EET by local organizers, ewscs08(at)cs.ioc.ee
EWSCS'08 page: http://cs.ioc.ee/ewscs/2008/