A relationship-based approach to the verification of multi-object invariants

Add to your list(s) Download to your calendar using vCal

• Stephanie Balzer, ETH Zurich
• Thursday 04 November 2010, 14:00-15:00
• Small lecture theatre, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

The object invariant has proved viable as a foundation for verifying object-oriented programs and is central to a wealth of object-oriented verification techniques. However, the presence of multi-object invariants and call-backs poses serious challenges for object invariant-based verification as they compromise modular verification and prohibit a naive adoption of a visible states semantics.

In this talk, we introduce Rumer, a relationship-based programming language that complements objects with first-class relationships. A relationship is a programming language abstraction that captures the interdependencies between objects. We discuss how relationships can aid in the modular verification of multi-object invariants. We introduce the “Matryoshka Principle”, a metaphor capturing Rumer’s key encapsulation properties that make the language amenable to modular verification. The principle stipulates restrictions on field and method access that translate into a stratification of the invariants imposed on a Rumer program. A verification technique can now leverage the invariant stratification as it allows restoring a visible states semantics for multi-object invariants. We elaborated a visible states verification technique for Rumer, which we outline in this talk.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Small lecture theatre, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.