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.
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.