Research

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

 

Centre for Cyber Trust

A verified security architecture. More

 

Gobra Logo

Gobra: A verifier for Go programs. More

 

Nagini

Nagini: A verifier for Python 3. More

prusti

A verifier for
Rust programs. More

VerifiedSCION

Formal verification of the SCION internet architecture implementation. More

Viper

A verification infrastructure for permission-based reasoning. More

Viper Roots

Viper Roots: Formal foundations of translational verifiers. More

 

Previous research projects

Chalice

An experimental language and verifier for concurrent programs. More

Envision

A fast and scalable visual programming interface. More

Heterogeneous Proof-Carrying Components

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

JIVE

Interactive verification of sequential Java programs.

Lyra

Static analysis for data science applications. More

Mobius - Mobility, Ubiquity, and Security

Correctness and security of mobile Java code.

Sample

A generic static analyzer based on abstract interpretation. More

Spec#

Integrating formal verification into mainstream programming languages. More

Tandem

Complementing partial verification results with automatic test case generation. More

TouchGuru

Integrating static analysis with a mobile development environment. More

Universe Type System

Controlling object structures by ownership. More

JavaScript has been disabled in your browser