Object Propositions

Speaker: Ligia Nistor , Oracle Labs

Date: Wednesday, April 09, 2014

Time: 2:30 PM to 3:30 PM Note: all times are in the Eastern Time Zone

Refreshments: 2:30 PM

Public: Yes

Location: 32-G882

Event Type:

Room Description:

Host: Adam Chlipala, CSAIL

Contact: Adam Chlipala, adamc@csail.mit.edu

Relevant URL:

Speaker URL: None

Speaker Photo:
None

Reminders to: seminars@csail.mit.edu, pl@csail.mit.edu

Reminder Subject: TALK: Object Propositions

The presence of aliasing makes modular verification of object-oriented
code difficult. If multiple clients depend on the properties of an
object, one client may break a property that others depend
on.
We have developed a modular verification approach based on the novel
abstraction of object propositions, which combine predicates
and information about object aliasing. In our methodology, even if
shared data is modified, we know that an object invariant specified by
a client holds. Our permission system allows verification using a mixture
of linear and nonlinear reasoning. We thus offer an alternative to separation logic verification approaches.
Object propositions can be more modular in some cases than separation logic because they can more effectively hide the exact aliasing relationships within a module. We validate the practicality of our approach by verifying an instance of the composite pattern. We implement our methodology in the intermediate verification language Boogie (of Microsoft Research), for the composite pattern example.

Research Areas:

Impact Areas:

See other events that are part of the PL/SE Seminar Series 2013/2014.

Created by Adam Chlipala at Thursday, March 13, 2014 at 6:01 PM.