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
A verifier for
Rust programs. More
Formal verification of the SCION internet architecture implementation. More
A verification infrastructure for permission-based reasoning. More
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