[Pl-seminar] 4/2: Ligia Nistor, Object Propositions

[Vincent St-Amour]

NUPRL Seminar presents

Ligia Nistor
Carnegie Mellon University

11:45 - 1:30
Wednesday, 4/2
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)


Object Propositions

Abstract: 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.

Bio: Ligia is a fifth year PhD student at Carnegie Mellon University's
Computer Science Department, working with Prof. Jonathan Aldrich. She is
currently ABD in absentia working for Oracle Corporation in Cambridge,
MA. Ligia is interested in formal methods, verification, programming
languages, and type systems. She has earned an MSc in Computer Science
from Oxford University in 2009. Her thesis was titled Model-Checking
Higher-Order Recursion Schemes.