 |
|
||||||||||
Universe Type System
Open Positions
We are recruiting PhD students in program verification, programming languages, and programming environments. Check out the job descriptions.
Our Mailing List
If you are interested in our activities, you can subscribe to the PMInterest mailing list.
Available Student Projects
Our group offers many different topics for Master's theses, Bachelor's theses, and Research in Computer Science Projects.
Object-oriented programs with arbitrary object structures are difficult to understand, to maintain, and to reason about since, in theory, all objects can interact with each other and methods might access any object in the heap memory via reference chains.
To support modular verification, especially of invariants, we developed a new programming model and type system for a subset of Java. This type system allows one to structure the heap memory into so-called universes and provides rigor, statically checkable control of references across universe boundaries. To make the universe type system available to a wider community and as a basis for case studies, we currently implement it as a part of the Java Modeling Language JML.
We are working on the static and dynamic inference of ownership properties in order to ease the transition from current Java programs to programs that use the Universe type system. To support modular inference of annotations we evaluate different possible extensions to the Universe type system. The introduction of type variables could allow partial inference of annotations.
Linked List
Results
We integrated the Universe type system into the MultiJava compiler and the JML Tools. We have a separate description of our tools.
Collaborations
We collaborate with the developers of the MultiJava compiler and the JML Tools. Special mention is due to Gary Leavens and Sophia Drossopoulou.
Project Members
Contact
Wichtiger Hinweis:
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
folgender
Seite.
Important Note:
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.
More
information
