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

[Vincent St-Amour]

At Wed, 19 Mar 2014 14:46:53 -0400,
Vincent St-Amour wrote:
> 
> 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.
> 
> _______________________________________________
> pl-seminar mailing list
> pl-seminar at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar