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.
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.
Diese Website wird in älteren Versionen von Netscape ohne graphische Elemente dargestellt. Die Funktionalität der Website ist aber trotzdem gewährleistet. Wenn Sie diese Website regelmässig benutzen, empfehlen wir Ihnen, auf Ihrem Computer einen aktuellen Browser zu installieren. Weitere Informationen finden Sie auf
The content in this site is accessible to any browser or Internet device, however, some graphics will display correctly only in the newer versions of Netscape. To get the most out of our site we suggest you upgrade to a newer browser.