We develop techniques and tools that exploit automated reasoning and large amounts of computing power to tackle challenging programming problems


Sketch — A synthesis-enabled language that allows programmers to write programs with holes and then rely on constraint-based synthesis to discover the missing code.
People: Armando Solar-Lezama

Jeeves — A programming language for automatically enforcing security and privacy policies.
People: Jean Yang

Bellmania — Deductive synthesis for large-scale implementations of dynamic programming algorithms. Strives to produce cache-oblivious distributed programs using a divide-and-conquer method. Incorporates modern proof techniques with a software refinement paradigm.
People: Shachar Itzhaky

Object Spreadsheets (joint work with SDG) — Attempts to make data-driven programming more accessible to end-users by imitating the look-and-feel of spreadsheets. The design comprises of a hybrid tabular-hierarchical data model, a query language for writing formulas, and an IDE.
People: Shachar Itzhaky, Matt McCutchen

Cyber-Physical Security — Safety-critical embedded systems are vulnerable to combinations of cyber and physical attacks. Examples include Stuxnet attacks on power grids and GPS spoofing. We use program analysis and synthesis techniques to analyze security vulnerability and develop defense mechanisms. People: Sicun Gao

Control Design Automation — To design controllers for dynamical systems is to solve a special class of program synthesis problems. We exploit the connection between control theory and formal methods to develop automated methods for hybrid and nonlinear control.
People: Sicun Gao

Synquid — Synquid stands for SYNthesis from liQUID types. It extends the Liquid Types framework, used successfully in program verification, to the domain of program synthesis, exploiting the combination of types and SMT-decidable predicates to generate provably correct programs in a modular fashion.
People: Nadia Polikarpova

Sigma — Sigma is a probabilistic programming language. It allows you to specify arbitrarily complex probabilistic models as functional programs, and provides inference procedures to answer questions about the model. Sigma’s inference algorithms combine modern statistical inference methods with abstract interpretation, SAT solving, and non-linear constraint solving.
People: Zenna Tavares

MSL — MSL is a synthesis enabled language for writing bulk-synchronous SPMD implementations.
People: Zhilei Xu

Cubix — Cubix is a framework for language-parametric source-to-source transformation. The ability to automatically rewrite code is critical for everything from automated refactoring to automated bug-fixing. Previous tools would need to be rewritten from scratch for each language because they lacked a way to handle the subtle variations between languages. We're making it possible to build tools that work on every language, and are just as good as tools written specifically for each language.
People: Jimmy Koppel

Mandate — If you write down the formal semantics of a programming language, it should be theoretically possible to automatically generate any tool you want for it. Mandate is a framework for doing this by performing rewrites and abstractions of rules. So far, we have focused on automatically synthesizing control-flow graph generators from operational semantics.
People: Jimmy Koppel

3cobblers — 3cobblers is an approximate program synthesis framework. Rather than synthesizing a correct program all at once, which can be difficult, it synthesizes a sequence of simpler approximate programs that approaches the correct program.
People: Evan Pu

AutoSMT — AutoSMT is a framework for automatically generating domain-specific rewriters for SMT problems. The generated problem rewriters are auto-tuned to performance of a specific solver for problems from a particular domain.
People: Rohit Singh



Osbert Bastani, UPenn

Nadia Polikarpova, UCSD

Sicun Gao, UCSD

Shachar Itzhaky, Technion

Rohit Singh, Uber

Xiaokang Qiu, Purdue University

Zhilei Xu, Google

Kuat Yessenov, Google

Jean Yang, Carnegie-Mellon University

Rishabh Singh, Google Brain

Alvin Cheung, University of Washington


If you are an MIT student and you are interested in working with us, check out our list of open UROP/MEng projects below.

Parametric Inversion of Non-Invertible Functions — We are developing exciting algorithms to run complicated programs backwards, literally. The goal is straightforward: to take a program (e.g. a rendering function which maps geometry to images), and construct an inverse program (e.g. which maps images to geometry). Executing a program backwards is non-trivial, so we apply a combination of semantic program analysis and machine learning to help. We have a number of possible projects for a UROP:

The greater your skill set and interests overlap with the following set, the stronger we urge you to get in touch: {program analysis, (deep) machine learning, probabilistic inference, computer graphics, planning, reinforcement learning, constraint solving}


Contact: Zenna Tavares

Reading Programmer's Minds for Smart Renaming

Suppose you have a codebase, and you want to rename all the Kitten's to Cat's. Easy — find and replace, right? But what about if you have a variable named "k" or "kt," or a class called "KName" — should you rename those? There's no mechanical rule to decide, and, as a result, many codebases still have remnants of names that were last used a decade ago.

We want to make a smart renaming tool that can figure out what else to rename when you rename a concept. We have a crazy idea for how to do this. It's a blend of program synthesis and causal inference, with a smattering of algorithmic information theory and some optional probablistic modeling. Would you like to help?


Contact: James Koppel

Synthesizing Programming Tools from Language Semantics — Program analysis and synthesis tools are promising to make programming 100x easier. Yet today they're rarely used because they're very specialized yet expensive to build. A significant part of developing them lies in creating basic components to discover the structure of code, such as control-flow graph generators and type-checkers. In principle, however, if we start with a formal description of a programming language's semantics, we could generate all of these automatically. Towards that end, we are building Mandate, the world's first control-flow graph generator generator. Mandate inputs the formal semantics of a programming language, and outputs a control-flow graph generator for that language. This project can be a good way to learn Haskell and programming-language semantics. We have a number of possible projects for a UROP:


Contact: James Koppel

Automatically Learning Semantics from a Compiler

Our Mandate framework is bringing us to a world where, if you write down the semantics of a language, you can generate any tool you want for it.

Now, imagine you didn't have to write down the semantics?

If you have an interpreter or compiler for a language, then that theoretically already contains all the information about what programs in this language mean. Our goal for this project is to extract that information out and convert it to a human- and machine-readable form using program synthesis techniques.

This is a more advanced project for someone who wants to get chest-deep into program synthesis and learn some Haskell too.


Contact: James Koppel

Multi-Language Transformation — Program transformations power tools ranging from automated bug-fixing to migrating entire projects. We find ways of making tools using 10x less code that can be used by 10x more people. We've built ways of expressing program transformations at a higher level, so that they can run on multiple programming languages, while being just as good as ones built for each programming language (and can transform code better than humans, according to our study). We have a number of possible projects for a UROP: Our Cubix framework pushes the Haskell language to its limits, so, if you like Haskell, working on this project will take your Haskell skills into the sky. Knowledge of compilers will also be helpful.


Contact: James Koppel