Current Projects


Deep logical reasoning via neural learning.

Description: This project is investigating neural learning approaches to solve program reasoning tasks that require deep logical reasoning.

Example such tasks include program verification and program synthesis. A common characteristic of these tasks is the availability of an oracle to check a candidate solution, such as a proposed loop invariant in verification, or a proposed program in synthesis. This project is employing deep reinforcement learning to predict such candidates generated by a graph neural network.

We have demonstrated this approach for two challenging problems:

Members: Xujie Si, Hanjun Dai, Mukund Raghothaman, Yuan Yang, Mayur Naik, Le Song

Keywords: Deep Reinforcement Learning, Graph Neural Networks, Program Verification, Program Synthesis

Sponsor: NSF award [1, 2], Facebook research award


General-purpose software debloating.

Description: Prevalent software engineering practices have significantly increased the complexity and bloat of today's software. This in turn has led to decreased performance and increased security vulnerabilities. The Chisel project seeks to effectively counter this trend.

Unlike conventional programming tools, which seek to preserve the program’s behavior, Chisel alters the program's behavior by removing unnecessary functionality. The project is addressing a multitude of research problems such as how to specify the desired behavior, how to efficiently debloat programs in language-specific and language-independent ways, and what correctness guarantees to provide.

Chisel curently supports the C family of languages.

Links: [CCS 2018 paper] [Chisel tool]

Members: Pardis Pashakhanloo, Kihong Heo, Woosuk Lee, Mayur Naik

Keywords: Program Transformation, Software Customization, Complexity Reduction, Security Hardening

Sponsor: ONR TPCP


AI-based program analysis framework.

Description: This project seeks to achieve a quantum leap in accuracy of static code analyses that target discovering deep semantic bugs and security vulnerabilities in large C/C++ programs. The key insight is to rank analysis alarms by performing inference on a conventional graphical model (e.g., a Bayesian network or a Markov logic network) that quantifies the incompleteness in individual steps of reasoning of the analysis.

Here is a video demo showing an application of this approach to interactively finding insidious datarace bugs in a large Java program.

Links: [PLDI 2018 paper] [source code]

Members: Sulekha Kulkarni, Kihong Heo, Mukund Raghothaman, Mayur Naik

Keywords: Program Analysis, Graphical Models of Code, Probabilistic Analysis of Programs, Big Code

Sponsors: DARPA MUSE, NSF (award abstract), Facebook research award


Learning-based optimizer for mobile apps.

Description: Inspired by the Google Build for Billions initiative, which considers program development techniques with emerging markets in mind, this project aims to automatically optimize rich mobile applications with respect to increasing demands on network data, memory, and processing capabilities. We are addressing how to leverage machine learning and end-users to effectively guide such optimizations.

Members: Brian Heath, Neelay Velingker, Osbert Bastani, Mayur Naik

Keywords: Performance Optimization, Specification Learning, Mobile Applications

Sponsor: ONR TPCP

Former Projects

a mobile-cloud computing platform

configurable program analysis

a program analysis platform for Java

automated testing of smartphone apps

analysis of concurrent programs