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



Static analysis of data science applications. More


Formal analysis of smart contracts. 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

Formal verification of the SCION internet architecture implementation. 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 Jun 23 10:01:29 CEST 2017
© 2017 Eidgenössische Technische Hochschule Zürich