Main content

The objective of our research is to create techniques and tools for the development of high-quality software, in particular, provably correct object-oriented programs. To achieve this goal, we study and apply a variety of approaches including program specification and verification, advanced type systems, static analysis, and testing. We are particularly interested in combining different approaches to develop techniques that are powerful and practical.

Current research projects


An experimental language and verifier for concurrent programs. More


A fast and scalable visual programming interface. More


A generic static analyzer based on abstract interpretation. More


Integrating formal verification into mainstream programming. More


Complementing partial verification results with automatic test case generation. More


Integrating static analysis with a mobile development environment. More


A verification infrastructure for permission-based reasoning. More

Previous research projects

Heterogeneous Proof-Carrying Components

Proof-Carrying Code for functional correctness properties in multi-language environments


Interactive verification of sequential Java programs

Mobius - Mobility, Ubiquity, and Security

Correctness and security of mobile Java code

Universe Type System

Controlling object structures by ownership

Page URL:
Fri May 27 07:59:54 CEST 2016
© 2016 Eidgenössische Technische Hochschule Zürich