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

DemoMatch — Have you ever seen an app do something and thought “I want my app to do that too?” DemoMatch gives you a tutorial for doing something with a framework simply by observing another program doing so.
People: Kuat Yessenov, Jimmy Koppel

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

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



Rishabh Singh, Microsoft Research

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 project below.

Synthesis of Functional Programs with Refinement Types — We are developing Synquid: a tool that automatically synthesizes recursive functional programs given a specification in the form of a refinement type. For example, you can ask Synquid to generate a function that deletes a value x from a list xs by specifying its refinement type as x: a -> xs: [a] -> {v: [a] | elems v = elems xs - {x}}.
The student will create benchmarks and case studies to help us explore the advantages and limitations of this approach to program synthesis and evaluate the usefulness of Synquid in practice. Another possible project direction is to create a web interface for Synquid along the lines of the Hoogle search engine in order to make the synthesizer easily accessible to developers.


Contact: Nadia Polikarpova

Weakest Preconditions for LiquidHaskellLiquidHaskell is a static verifier for Haskell developed at UCSD. LiquidHaskell can verify complex functional programs completely automatically using a technique called Liquid Type Inference, which combines refinement types, predicate abstraction, and SMT solving.
When the program under verification consists of multiple functions, Liquid Haskell infers pre- and postconditions for those functions. One current limitation is that the inferred precondition for a function f depends on the call sites of f; thus, adding a new call site can affect the inferred precondition and trigger a verification error in an unrelated part of the program. This makes the verifier's behavior unpredictable and impairs its usability.
Addressing this problem calls for inferring the "weakest" or "most general" precondition, which is independent from the function call sites. Unfortunately, such weakest precondition is often not unique, and finding all weakest preconditions is computationally expensive. A possible workaround is to allow the user to interact with the system and decide which of the inferred preconditions is the intended one. In this project the student will integrate weakest precondition inference into LiquidHaskell, evaluate its applicability to real-world examples, and implement a GUI to enable user interaction.


Contact: Nadia Polikarpova