Mining and Understanding Bug Fixes for App-Framework Protocol Defects

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

A Framework Model for Static Analysis of Android Applications

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.

References: SOAP 2015
QUIC Graphs
Relational Invariant Generation for Containers

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

References: ECOOP 2013
Precise Refutations for Heap Reachability

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

References: PLDI 2013
Fissile Type Analysis
Modular Checking of Almost-Everywhere Invariants

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

References: POPL 2014