BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A relationship-based approach to the verification of multi-object 
 invariants - Stephanie Balzer\, ETH Zurich
DTSTART:20101104T140000Z
DTEND:20101104T150000Z
UID:TALK27853@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:The object invariant has proved viable as a foundation for ver
 ifying object-oriented programs and is central to a wealth of object-orien
 ted verification techniques.  However\, the presence of multi-object invar
 iants and call-backs poses serious challenges for object invariant-based v
 erification as they compromise modular verification and prohibit a naive a
 doption of a visible states semantics.\n\nIn this talk\, we introduce Rume
 r\, a relationship-based programming language that complements objects wit
 h first-class relationships.  A relationship is a programming language abs
 traction that captures the interdependencies between objects.  We discuss 
 how relationships can aid in the modular verification of multi-object inva
 riants.  We introduce the "Matryoshka Principle"\, a metaphor capturing Ru
 mer's key encapsulation properties that make the language amenable to modu
 lar verification.  The principle stipulates restrictions on field and meth
 od access that translate into a stratification of the invariants imposed o
 n a Rumer program.  A verification technique can now leverage the invarian
 t stratification as it allows restoring a visible states semantics for mul
 ti-object invariants.  We elaborated a visible states verification techniq
 ue for Rumer\, which we outline in this talk.
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR