Current projects

Hyperkernel A push-button approach to building provably correct OS kernels.
Rosette A programming language for building verification and synthesis tools.
SymPro A profiler for identifying and diagnosing performance bottlenecks in programs under symbolic evaluation.
Yggdrasil A toolkit for writing file systems with push-button verification.

Past projects

Ferrite A framework for specifying and checking file system crash-consistency models.
MemSynth A language and tool for verifying, synthesizing, and disambiguating memory consistency models.
Neutrons A verifier for a subset of EPICS. Currently in use at the University of Washington Clinical Neutron Therapy System.
Synapse A framework for specifying and solving optimal synthesis problems.