CMU-CS-17-132
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-17-132

Object Propositions

Ligia Nicoleta Nistor

January 2018

Ph.D. Thesis

CMU-CS-17-132.pdf


Keywords: Verification, Java, Oprop, logic, Boogie

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.

In this thesis we present 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. This allows it to provide more modularity in some cases than competing separation logic approaches, because it can more effectively hide the exact aliasing relationships within a module. We have implemented the methodology into our tool Oprop. We have used Oprop to automatically verify a number of examples, thus showing the applicability of this research.

197 pages

Thesis Committee:
Jonathan Aldrich (Chair)
Frank Pfenning
David Garlan
Matthew Parkinson (Microsoft Research)

Frank Pfenning, Head, Computer Science Department
Andrew W. Moore, Dean, School of Computer Science




Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu