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.
The goal of the Semper project is to build an automatic program verifier for Scala programs. Some of the key research challenges that we are currently exploring are: (1) how to automatically verify concurrent programs that make use of a variety of idioms, in particular, actors; (2) how to effectively reduce the annotation overhead by integrating the verifier with a powerful contract inference; and (3) how to reason about the functional features of Scala such as closures using automatic theorem provers.
The verification methodology used in Semper is based on Chalice. The inference is performed by our generic abstract interpreter Sample, which can be instantiated with various custom analyses.
Semper is a new project. Initial results include a verification methodology for closures, a new specification methodology based on fractional permissions, static analyses for pattern matching, information flow, and string values, and an automatic inference of access permissions.
We collaborate with the group of Tino Cortesi, Universita` Ca' Foscari, Venezia, on static analysis.
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.