University of Cambridge > > Microsoft Research Cambridge, public talks > A relationship-based approach to the verification of multi-object invariants

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

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2022, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity