Projects

We develop the foundations and tools needed to build reliable software and secure hardware. Our projects combine programming languages, formal methods, and systems research.

Concurrency

Algorithms and tools for testing and verifying concurrent software, with a focus on race detection, predictive analysis, fuzzing, and weak memory.

Formal Methods for Secure Hardware Design

Languages, type systems, and verification techniques for building safe and secure hardware, including Anvil and its guarantees against timing hazards.