Developing program analysis, probabilistic inference, program synthesis, social data mining, and big-data engineering tools to cooperative repair Android framework protocol misuses.

A community-driven modeling of the Android framework for static analysis of Android applications. Droidel seeks to be a general purpose model for static analysis based on minimal explication of dynamism in the Android framework code.

An abstract domain constructor for inferring invariants about sets and set properties of containers.

A static analysis tool for Java programs that specializes in checking heap reachability properties and provides automated alarm triage assistance.

A static analysis tool for C and Objective-C that verifies invariants that hold almost everywhere, including the safety of reflective method calls.