Research

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

JIVE

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: http://www.pm.inf.ethz.ch/research.html
Tue Jun 28 11:35:04 CEST 2016
© 2016 Eidgenössische Technische Hochschule Zürich