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:
Loop invariants for program verification.
Syntax-guided program synthesis (SyGuS).
Links: [ICLR 2019 paper]
Keywords: Deep Reinforcement Learning, Graph Neural Networks, Program Verification, Program Synthesis
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.
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.
Keywords: Program Analysis, Graphical Models of Code, Probabilistic Analysis of Programs, Big Code
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.
Keywords: Performance Optimization, Specification Learning, Mobile Applications
Sponsor: ONR TPCP
a mobile-cloud computing platform
configurable program analysis
a program analysis platform for Java