Apply to CS
Apply to ECE
Some of our group's research projects.
: a tool to build sound and precise call graphs for an application without analyzing the whole program
The Checker Framework
: a framework to build pluggable type systems for Java, including example type systems like the Nullness Checker and the Regex Checker.
: a tool for improving the precision of static data-flow analysis for object-oriented programs; comes with an implementation of the
: A declarative programming language for fixpoints on lattices.
Mining and understanding software enclaves (MUSE)
subcontract: inferring properties from large code repositories.
Static Program Analysis for Reliable Trusted Apps (SPARTA)
: information flow verification for mobile devices.
: crowd-sourced program verification.