The Relationship Between Ownership and Implicit Dynamic Frames

Introduction

Ownership provides a means for structuring programs, in a way which facilitates reasoning about object invariants. The Spec# verifier's approach to object invariants is based on such a notion of ownership, which controls which objects can be modified at which program points. On the other hand, Chalice is a verification tool for concurrent programming, which controls which objects can be modified via the notion of access permissions in specifications (the corresponding assertion language is called Implicit Dynamic Frames). Specifications using permissions are generally more flexible but also more verbose than those written in the presence of an ownership type system.

Goal

The goal of this project is to develop a verification technique which combines the two approaches of ownership (as used in Spec#) and permissions (as used in Chalice). This will allow programmers to choose the methodology which is most appropriate for each part of their program design, allowing flexibility where necessary, and succinct specifications where ownership can be used. This approach should be implemented in an extension of the Chalice tool, which will support Spec#-style ownership annotations. This project will involve investigating the relationship between the existing approaches, and designing and implementing a new methodology supporting the combination of both approaches together in the same program.

Since Chalice is being developed as an open-source project, the resulting compiler extensions should be contributed to the Chalice community. This requires that the extensions are well documented, thoroughly tested and implemented using good software engineering practices.

Recommended Background

• Concepts of Object-Oriented Programming
• Formal Methods
• Programming Experience (especially Compiler Construction)

Contact

Alex Summers or Valentin Wüstholz